2 papers
cs.LG2026
Escaping the Cognitive Well: Efficient Competition Math with Off-the-Shelf Models
Xingyu Dang, Rohit Agarwal, Rodrigo Porto +3
In the past year, custom and unreleased math reasoning models reached gold medal performance on the International Mathematical Olympiad (IMO). Similar performance was then reported…
cs.AI2026
Goedel-Architect: Streamlining Formal Theorem Proving with Blueprint Generation and Refinement
Jui-Hui Chung, Ziyang Cai, Zihao Li +14
We introduce Goedel-Architect, an agentic framework for formal theorem proving in Lean 4 centered on blueprint generation and refinement. A blueprint is a dependency graph of defin…