The system used a custom harness to generate proof strategies, coordinate subagents, manage distributed compute and API limits, search cached lemmas, and generate counterexamples with parallel C++ programs.
Loeber writes that GPT-5.5 could produce novel theorem work but was slow and often generated incorrect or incoherent statements. He says GPT-5.6 Sol improved proof strategies, and GPT-6 Astra improved them again. His project produced a few hundred thousand lines of Lean while working on the degree-57 Moore graph problem and the Hadwiger Conjecture.
The October 22, 2026 essay argues that base-model progress rapidly reduced the value of his specialized proof-search engineering. It also reports claims about an unreleased OpenAI model, a 4,000-problem run, and mathematical results by others. The essay does not provide independently inspectable evidence for those claims, the reported compute cost, or the correctness and novelty of the cited proofs.