Munkres' General Topology Autoformalized in Isabelle/HOL
Dustin Bryant, Jonathan Julián Huerta y Munive, Cezary Kaliszyk, Josef Urban
AI use, as the source states it
“We describe an experiment in LLM-assisted autoformalization that produced over 85,000 lines of Isabelle/HOL code covering all 39 sections of Munkres' Topology (general topology, Chapters 2--8), from topological spaces through dimension theory.”
Model: ChatGPT 5.2, Claude Opus 4.6, as stated
Named here, or see a mistake? Write to privacy@papex.org.