Junaid Hasan
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.
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.