The history of the additional extension work for Codex has been recorded here:
DkMath — Verifiable AI Mathematical Research
An auditable human–GPT-5.6–Codex workflow that extends a large Lean 4 mathematics library, verifies new prime/GN theorems, and turns proofs into reproducible visual demos.
Log in or sign up for Devpost to join the conversation.