Junaid Hasan Junaid Hasan

Blog

July 2026 IMO 2026 in Lean: GPT-5.6 Sol and AxiomProver

I gave the six formal statement files to GPT-5.6 Sol in Ultracode mode, with web search, GitHub, published solutions, and the other problem files explicitly forbidden. The runs were attempted in the order P1, P4, P5, P6, P2, P3; P3 took 1 hour 58 minutes. The article presents the mathematics of both the GPT and AxiomProver proofs and compares their ideas.

Read the article | PDF | GPT repository | Axiom repository

June 2026 I defended my thesis today.

I presented my thesis today. A recorded version is available at YouTube.

Along the way I built a few interactive demos to make the core ideas more tangible.