Create accountLogin

Recent searches

No recent searches

Search options

Only available when logged in.
mathstodon.xyz is one of the many independent Mastodon servers you can use to participate in the fediverse.
A Mastodon instance for maths people. We have LaTeX rendering in the web interface!

Administered by:

Server stats:

3.1K
active users

mathstodon.xyz: AboutStatusProfiles directoryPrivacy policy

Mastodon: AboutGet the appKeyboard shortcutsView source codev4.3.6

#leanprover

16 posts7 participants0 posts today
Public
Lean

Leo's talk, Verified Collaboration, presented as part of the Simon's Foundation Presidential Lecture series on mathematics and computer science has recently been posted.

Watch it here: youtube.com/watch?v=rmMYFmlUbJ8

There are some great examples of cross-disciplinary collaborative efforts highlighted, including the Liquid Tensor Experiment and SampCert, which Leo notes would have been impossible with the strength of Mathlib and the #LeanProver community behind it.

YouTubeLeonardo de Moura - Verified Collaboration: How Lean is Transforming Math...(March 12, 2025)By Simons Foundation
Public
José A. Alonso

Formalization of optimality conditions for smooth constrained optimization problems. ~ Chenyi Li et als. arxiv.org/abs/2503.18821

arXiv logo
arXiv.orgFormalization of Optimality Conditions for Smooth Constrained Optimization ProblemsOptimality conditions are central to analysis of optimization problems, characterizing necessary criteria for local minima. Formalizing the optimality conditions within the type-theory-based proof assistant Lean4 provides a precise, robust, and reusable framework essential for rigorous verification in optimization theory. In this paper, we introduce a formalization of the first-order optimality conditions (also known as the Karush-Kuhn-Tucker (KKT) conditions) for smooth constrained optimization problems by beginning with concepts such as the Lagrangian function and constraint qualifications. The geometric optimality conditions are then formalized, offering insights into local minima through tangent cones. We also establish the critical equivalence between the tangent cone and linearized feasible directions under appropriate constraint qualifications. Building on these key elements, the formalization concludes the KKT conditions through the proof of the Farkas lemma. Additionally, this study provides a formalization of the dual problem and the weak duality property.
Public
José A. Alonso

Formalization of algorithms for optimization with block structures. ~ Chenyi Li, Zichen Wang et als. arxiv.org/abs/2503.18806

arXiv logo
arXiv.orgFormalization of Algorithms for Optimization with Block StructuresBlock-structured problems are central to advances in numerical optimization and machine learning. This paper provides the formalization of convergence analysis for two pivotal algorithms in such settings: the block coordinate descent (BCD) method and the alternating direction method of multipliers (ADMM). Utilizing the type-theory-based proof assistant Lean4, we develop a rigorous framework to formally represent these algorithms. Essential concepts in nonsmooth and nonconvex optimization are formalized, notably subdifferentials, which extend the classical differentiability to handle nonsmooth scenarios, and the Kurdyka-Lojasiewicz (KL) property, which provides essential tools to analyze convergence in nonconvex settings. Such definitions and properties are crucial for the corresponding convergence analyses. We formalize the convergence proofs of these algorithms, demonstrating that our definitions and structures are coherent and robust. These formalizations lay a basis for analyzing the convergence of more general optimization algorithms.
Public
José A. Alonso

Teaching "Foundations of Mathematics" with the Lean theorem prover. ~ Mattia Luciano Bottoni, Alberto Cattaneo, Elif Sacikara. arxiv.org/abs/2501.03352v1

arXiv logo
arXiv.orgTeaching "Foundations of Mathematics" with the LEAN Theorem ProverThis study aims to observe if the theorem prover LEAN positively influences students' understanding of mathematical proving. To this end, we perform a pilot study concerning freshmen students at the University of Zurich (UZH). While doing so, we apply certain teaching methods and gather data from the volunteer students enrolled in the ``Foundations of Mathematics'' course. After eleven weeks of study covering some exercise questions implemented with LEAN, we measure LEAN students' performances in proving mathematical statements, compared to other students who are not engaged with LEAN. For this measurement, we interview five LEAN and four Non-LEAN students and we analyze the scores of all students in the final exam. Finally, we check significance by performing a $t$-test for independent samples and the Mann-Whitney $U$-test.
SearchLive feeds
About