/AI6h ago

Open-Source Goedel-Architect Framework Achieves SOTA Lean 4 Theorem Proving Results

32411151.7K
#901Chi Jin
Jui-Hui Chung
Original postChi Jin#901
Jui-Hui Chung@juihuichung

Introducing Goedel-Architect: an open-source framework for formal theorem proving in Lean 4. Using the open-weight DeepSeek-V4-Flash (284B-A13B), it reaches state-of-the-art results, rivaling proprietary systems at a fraction of the cost.

It solves 4/6 on IMO 2025, 11/12 on Putnam 2025, and 3/6 on USAMO 2026. On PutnamBench it solves 88.8% (597/672) at just ~$1.65 per problem.

Paper: https://arxiv.org/abs/2606.06468 Project page: https://goedelarchitect.github.io/

9:33 AM · Jun 8, 2026 · 1.7K Views
Sentiment

Users thank their collaborators for creating the Goedel-Architect open-source framework that sets a new SOTA in Lean 4 theorem proving.

Pos
100.0%
Neg
0.0%
1 comments with sentiment.
Cluster Engagement
Posts from X
Most Activity
Most Activity
VIEWS55
Jui-Hui Chung@juihuichung

The core idea is a blueprint: a global dependency graph of lemmas that build up to the theorem. The lemmas are proved in parallel, and any failures feed back to refine the graph.

6hViews 55
Jui-Hui Chung@juihuichung

Huge thanks to my amazing collaborators: @jackcai1206, @Zi_Hao_Li, @qishuo_yin, @Rohit_Writes, @parksimon0808, Rodrigo Porto, @narutatsuri, @__zrrr__, @sangertang1999, @xingyudang, @hongzhou__lin, @MengdiWang10, @danqi_chen, @chijinML, Liam Fowl, @prfsanjeevarora

6hViews 48