José A. AlonsoReadings shared March 14, 2026. https://jaalonso.github.io/vestigium/posts/2026/03/15-readings_shared_02-14-26 #AI #Agda #ITP #LeanProver #Math #Mizar
Optimal Caverna gameplay via formal methods. ~ Stephen Diehl. https://www.stephendiehl.com/posts/caverna/ #LeanProver #ITP
Duality theory in linear optimization and its extensions - formally verified. ~ Martin Dvorak, Vladimir Kolmogorov. https://afm.episciences.org/17678 #LeanProver #ITP #Math
Duality theory in linear optimization and its extensions -- formally verified
Farkas established that a system of linear inequalities has a solution if and only if we cannot obtain a contradiction by taking a linear combination of the inequalities. We state and formally prove several Farkas-like theorems over linearly ordered fields in Lean 4. Furthermore, we extend duality theory to the case when some coefficients are allowed to take "infinite values".
A formalization of Borel determinacy in Lean. ~ Sven Manthe. https://afm.episciences.org/17712 #LeanProver #ITP #Math
A formalization of Borel determinacy in Lean
We present a formalization of Borel determinacy in the Lean 4 theorem prover. The formalization includes a definition of Gale-Stewart games and a proof of Martin's theorem stating that Borel games are determined. The proof closely follows Martin's "A purely inductive proof of Borel determinacy".
From SMT solvers to Lean and the future of automated reasoning. ~ Leo de Moura, Nicola Gigante. https://etaps.org/blog/043-leo-de-moura/ #LeanProver #ITP
Joachim BreitnerRE: https://discuss.systems/@bobkonf/116221261428106677
I showed up this morning at breakfast at #bobkonf looking forward to some relaxed listening to tasks, when the organizer approached me and asked if can spontaneously fill a slot. So I did and gave a #leanProver talk. This keeps happening to me, that's how I ended up giving a talk here last year 🤷🏻
Formalizing research #mathematics with #leanprover is normal these days, but now people are formalizing #physics results as well, to bring it up to that level of rigor – and already the first paper they look at falls apart, with the main theorem being (provably) incorrect: https://arxiv.org/abs/2603.08139
Formalizing the stability of the two Higgs doublet model potential into Lean: identifying an error in the literature
In 2006, using the best methods and techniques available at the time, Maniatis, von Manteuffel, Nachtmann and Nagel published a now widely cited paper on the stability of the two Higgs doublet model (2HDM) potential. Twenty years on, it is now easier to apply the process of formalization into an interactive theorem prover to this work thanks to projects like Mathlib and PhysLib (formerly PhysLean and Lean-QuantumInfo), and to ask for a higher standard of mathematical correctness. Doing so has revealed an error in the arguments of this 2006 paper, invalidating their main theorem on the stability of the 2HDM potential. This case is noteworthy because to the best of our knowledge it is the first non-trivial error in a physics paper found through formalization. It was one of the first papers where formalization was attempted, which raises the uncomfortable question of how many physics papers would not pass this higher level of scrutiny.
Fantastic simprocs and how to write them. ~ Yaël Dillies, Paul Lezeau. https://leanprover-community.github.io/blog/posts/simprocs-tutorial/ #LeanProver #ITP
Formalizing the stability of the two Higgs doublet model potential into Lean: identifying an error in the literature. ~ Joseph Tooby-Smith. https://arxiv.org/abs/2603.08139v1 #LeanProver #ITP #Physics
Formalizing the stability of the two Higgs doublet model potential into Lean: identifying an error in the literature
In 2006, using the best methods and techniques available at the time, Maniatis, von Manteuffel, Nachtmann and Nagel published a now widely cited paper on the stability of the two Higgs doublet model (2HDM) potential. Twenty years on, it is now easier to apply the process of formalization into an interactive theorem prover to this work thanks to projects like Mathlib and PhysLib (formerly PhysLean and Lean-QuantumInfo), and to ask for a higher standard of mathematical correctness. Doing so has revealed an error in the arguments of this 2006 paper, invalidating their main theorem on the stability of the 2HDM potential. This case is noteworthy because to the best of our knowledge it is the first non-trivial error in a physics paper found through formalization. It was one of the first papers where formalization was attempted, which raises the uncomfortable question of how many physics papers would not pass this higher level of scrutiny.