#LeanProver

@jalonso.eurosky.social

2 hours ago

Readings shared March 14, 2026 The readings shared in Bluesky on 14 March 2026 are: From SMT solvers to Lean and the future of automated reasoning. ~ Leo de Moura, Nicola Gigante. #LeanProver #ITP A formalization of Borel determin

Readings shared March 14, 2026. jaalonso.github.io/vestigium/po... #AI #Agda #ITP #LeanProver #Math #Mizar

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

15 hours ago

Optimal Caverna Gameplay via Formal Methods - Stephen Diehl Personal blog of Stephen Diehl - Software engineer writing about technology, programming, and the future

Optimal Caverna gameplay via formal methods. ~ Stephen Diehl. www.stephendiehl.com/posts/caverna/ #LeanProver #ITP

0 1 0 0

José A. Alonso

@jalonso.eurosky.social

15 hours ago

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".

Duality theory in linear optimization and its extensions - formally verified. ~ Martin Dvorak, Vladimir Kolmogorov. afm.episciences.org/17678 #LeanProver #ITP #Math

1 0 0 0

José A. Alonso

@jalonso.eurosky.social

15 hours ago

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".

A formalization of Borel determinacy in Lean. ~ Sven Manthe. afm.episciences.org/17712 #LeanProver #ITP #Math

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

15 hours ago

From SMT Solvers to Lean and the Future of Automated Reasoning Interview with Leo De Moura about his career and his work on Lean.

From SMT solvers to Lean and the future of automated reasoning. ~ Leo de Moura, Nicola Gigante. etaps.org/blog/043-leo... #LeanProver #ITP

2 1 0 0

José A. Alonso

@jalonso.eurosky.social

4 days ago

Readings shared March 9, 2026 The readings shared in Bluesky on 9 March 2026 are: Fantastic simprocs and how to write them. ~ Yaël Dillies, Paul Lezeau. #LeanProver #ITP Formalization in Lean of faithfully flat descent of project

Readings shared March 09, 2026. jaalonso.github.io/vestigium/po... #AI #AI4Math #CategoryTheory #CoqProver #Emacs #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LambdaCalculus #LeanProver #Lisp #Math #Physics #RocqProver

2 0 0 0

José A. Alonso

@jalonso.eurosky.social

5 days ago

Fantastic Simprocs and How to Write Them How to write a simproc in practice

Fantastic simprocs and how to write them. ~ Yaël Dillies, Paul Lezeau. leanprover-community.github.io/blog/posts/s... #LeanProver #ITP

7 1 0 0

José A. Alonso

@jalonso.eurosky.social

5 days ago

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 (...

Formalizing the stability of the two Higgs doublet model potential into Lean: identifying an error in the literature. ~ Joseph Tooby-Smith. arxiv.org/abs/2603.081... #LeanProver #ITP #Physics

2 1 0 0

José A. Alonso

@jalonso.eurosky.social

5 days ago

Implementing Dependent Type Theory Inhabitation and Unification Dependent type theory is the foundation of many modern proof assistants. Inhabitation and unification are undecidable problems that are useful for theorem proving and program synthesis. We introduce C...

Implementing dependent type theory inhabitation and unification. ~ Chase Norman, Jeremy Avigad. arxiv.org/abs/2603.01463 #LeanProver #ITP

4 1 0 0

José A. Alonso

@jalonso.eurosky.social

5 days ago

Unbiasing symmetric monoidal categories in Lean We present a formalization in Lean 4, within the framework of the mathematical library Mathlib, of the unbiasing process for symmetric monoidal categories. This is realized by extending the data of a ...

Unbiasing symmetric monoidal categories in Lean. ~ Robin Carlier. arxiv.org/abs/2603.00896 #LeanProver #ITP

1 0 0 0

José A. Alonso

@jalonso.eurosky.social

5 days ago

Mathematicians in the age of AI Recent developments show that AI can prove research-level theorems in mathematics, both formally and informally. This essay urges mathematicians to stay up-to-date with the technology, to consider the...

Mathematicians in the age of AI. ~ Jeremy Avigad. arxiv.org/abs/2603.03684 #AI4Math #LeanProver #ITP

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

5 days ago

Formalization in Lean of faithfully flat descent of projectivity We formalize in Lean the following foundational result in commutative algebra: Let $R \to S$ be a faithfully flat map of (not necessarily noetherian) commutative rings, and let $P$ be an arbitrary $R$...

Formalization in Lean of faithfully flat descent of projectivity. ~ Liran Shaul. arxiv.org/abs/2603.04376 #LeanProver #ITP

1 0 0 0

José A. Alonso

@jalonso.eurosky.social

5 days ago

Formalizing unstable quasinormal modes and the quantum black hole bomb in Lean 4. ~ Naoki Takata. naokitakata.com/quantum_supe... #ITP #LeanProver

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

5 days ago

Shaping the future of mathematics in the age of AI. ~ Johan Commelin, Mateja Jamnik, Rodrigo Ochigame, Lenny Taelman, Akshay Venkatesh. www.math.ias.edu/~akshay/mnot... #AI4Math #LeanProver #ITP

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

5 days ago

Category Theory for Programming In these lecture notes, we give a brief introduction to some elements of category theory. The choice of topics is guided by applications to functional programming. Firstly, we study initial algebras, ...

Category theory for programming. ~ Benedikt Ahrens, Kobe Wullaert. arxiv.org/abs/2209.012... #CategoryTheory #Haskell #LeanProver #FunctionalProgramming

4 0 1 0

José A. Alonso

@jalonso.eurosky.social

5 days ago

LeanTutor: A Formally-Verified AI Tutor for Mathematical Proofs We present LeanTutor, a Large Language Model (LLM)-based tutoring system for math proofs. LeanTutor interacts with the student in natural language, formally verifies student-written math proofs in Lea...

LeanTutor: A formally-verified AI tutor for mathematical proofs. ~ Manooshree Patel, Rayna Bhattacharyya, Thomas Lu, Arnav Mehta, Niels Voss, Narges Norouzi, Gireeja Ranade. arxiv.org/abs/2506.083... #LeanProver #ITP #Math #AI4Math

1 0 0 0

José A. Alonso

@jalonso.eurosky.social

5 days ago

Formalizing a proof in Lean using Claude Code YouTube video by Terence Tao

Formalizing a proof in Lean using Claude Code. ~ Terence Tao. youtu.be/JHEO7cplfk8 #LeanProver #ITP #AI4Math

3 0 1 0

José A. Alonso

@jalonso.eurosky.social

1 week ago

Readings shared March 4, 2026 The readings shared in Bluesky on 4 March 2026 are: When AI writes the world’s software, who verifies it? ~ Leonardo de Moura. #AI #LeanProver #ITP Formalising sphere packing in Lean. ~ Chris Birkbec

Readings shared March 04, 2026. jaalonso.github.io/vestigium/po... #AI #AI4Math #CoqProver #FunctionalProgramming #Haskell #ITP #LeanProver #Math #RocqProver

1 0 0 0

José A. Alonso

@jalonso.eurosky.social

1 week ago

ReasBook is a Lean 4 project for formalizing mathematics from textbooks and research papers. github.com/optpku/ReasB... #LeanProver #ITP #Math

2 2 0 0

José A. Alonso

@jalonso.eurosky.social

1 week ago

SorryDB: Can AI Provers Complete Real-World Lean Theorems? We present SorryDB, a dynamically-updating benchmark of open Lean tasks drawn from 78 real world formalization projects on GitHub. Unlike existing static benchmarks, often composed of competition prob...

SorryDB: Can AI provers complete real-world Lean theorems? ~ Austin Letson et als. arxiv.org/abs/2603.026... #LeanProver #ITP #AI

2 1 0 1

José A. Alonso

@jalonso.eurosky.social

1 week ago

The Purpose of Proofs In discussions of AI and Mathematics, the discussion often goes to mathematical proofs, such as the the First Proof challenge. So let's lo...

The purpose of proofs. ~ Lance Fortnow. blog.computationalcomplexity.org/2026/03/the-... #LeanProver #ITP #AI4Math

4 1 0 0

José A. Alonso

@jalonso.eurosky.social

1 week ago

Completing the formal proof of higher-dimensional sphere packing — Math, Inc. Dedicated to verified superintelligence via autoformalization.

Completing the formal proof of higher-dimensional sphere packing. www.math.inc/sphere-packing #LeanProver #ITP #AI4Math

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

1 week ago

The Sphere Packing Project | Post 1 - The Story The Sphere Packing Project maintainers tell the story of the project, up to the recent autoformalisation. This is the first of two blog posts that will discuss the recent formalisation of Viazovska'

The sphere packing project (Post 1: The story). ~ Chris Birkbeck Sidharth Hariharan Seewoo Lee. leanprover-community.github.io/blog/posts/S... #LeanProver #ITP #Math

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

1 week ago

Formalising sphere packing in Lean. ~ Chris Birkbeck, Sidharth Hariharan, Gareth Ma, Bhavik Mehta, Seewoo Lee, Maryna Viazovska. thefundamentaltheor3m.github.io/Sphere-Packi... #LeanProver #ITP #Math

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

1 week ago

When AI writes the world’s software, who verifies it? ~ Leonardo de Moura. leodemoura.github.io/blog/2026/02... #AI #LeanProver #ITP

1 1 0 0

ACP Section

@acp.mastodon.acm.org.ap.brid.gy

1 week ago

Original post on mastodon.acm.org

Anna Blume Jakobsen (www.daracademy.dk/current-fellows/anna-blu... joined ACP today. Her PhD project is on choreographic programming and cost semantics. Anna works on semantics, Lean formalisations, behavioural theory, and program optimisation.

#choreographicProgramming […]

1 1 0 0

José A. Alonso

@jalonso.eurosky.social

1 week ago

Readings shared March 1, 2026 The readings shared in Bluesky on 1 March 2026 are: Lean for science formalization. ~ Przemyslaw Chojecki. #LeanProver #ITP Vibe-coding a debugger for a DSL. ~ Joachim Breitner. #LeanProver Bidirecti

Readings shared March 01, 2026. jaalonso.github.io/vestigium/po... #ITP #LeanProver #RocqProver

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

1 week ago

Vibe-coding a debugger for a DSL. ~ Joachim Breitner. www.joachim-breitner.de/blog/819-Vib... #LeanProver

1 0 1 0

José A. Alonso

@jalonso.eurosky.social

1 week ago

Lean for science formalization. ~ Przemyslaw Chojecki. www.ulam.ai/research/lea... #LeanProver #ITP

1 0 0 0

Lean Focused Research Organization

@lean-lang.org

2 weeks ago

The Lean Y3 roadmap is building infrastructure to keep performance "visible and actionable." Radar automatically benchmarks every commit and compares it to previous ones to catch regressions and improvements.

See more: radar.lean-lang.org/about

#LeanLang #LeanProver

6 1 0 0

Posts tagged #LeanProver