Seonglae ChoTheorem prover
Leanstral
Leanstral: Open-Source foundation for trustworthy vibe-coding | Mistral AI
First open-source code agent for Lean 4.
https://mistral.ai/news/leanstral
Lean Programming Language
Lean is a theorem prover and programming language that enables correct, maintainable, and formally verified code.
https://lean-lang.org/
Seed-Prover
Formal languages like Lean enable automatic verification, making them advantageous for reinforcement learning (RL) through Lemma-Style Proving: proving intermediate lemmas first → utilizing them for main theorems, and Iterative Refinement: iteratively improving proofs using Lean feedback, self-summarization, and leveraging previous proofs.
www.arxiv.org
https://www.arxiv.org/pdf/2507.23726
FormalQualBenchp
FormalQualBench
FormalQualBench: 23 graduate-level theorems, formalized in Lean4, with comparator-verified benchmark results.
https://www.math.inc/formalqualbench
수학, 인공지능, 그리고 형식화 [2]: 증명의 형식화와 인공지능
앞에서 우리는 인공지능을 어떻게 수학 연구에 활용할 수 있는지에 대해서 알아보았습니다. 이번 편에서는 최근에 떠오르고 있는 증명의 형식화formalization에 대해서 알아보고, AI, 특히 LLM을 활용한 수학 연구에서의 형식화의 역할과 형식화에 있어서의 AI의 역할과 주의할 점에 대해서 알아보면서 이 시리즈를 마치고자 합니다. AI가 증명을 했다고 주장하는데, 확실한가요? 앞서 언급했듯이 ChatGPT Pro나 Gemini Deep Think 등 최전선에 있는…
https://horizon.kias.re.kr/33348/
![수학, 인공지능, 그리고 형식화 [2]: 증명의 형식화와 인공지능](https://horizon.kias.re.kr/wp-content/uploads/2027/04/FINAL_horizon8_1_600DPI-480x270.jpg)
Palomar – a registry of Lean verified mathematics
In recent months there has been a proliferation of AI-generated proofs of various old and new results, some of which have been formalized in the proof assistant language Lean. However, checking tha…
https://terrytao.wordpress.com/2026/08/18/palomar-a-registry-of-lean-verified-mathematics/
Leonardo de Moura
Leonardo de Moura
Leonardo de Moura is a Brazilian computer scientist, and creator of the Z3 Theorem Prover and the Lean proof assistant during his time at Microsoft Research. He currently works at AWS and is the Chief Architect at the Lean FRO.
https://en.wikipedia.org/wiki/Leonardo_de_Moura
