[submission] Abel–Ruffini — MathGraph + GPT-5.6 Sol

[heathsanchez]

Submission URL

https://github.com/metalogiclabs/mathgraph/tree/c6b90bfb7c2baf472cba66254f2bea6b70e5885a

Model

MathGraph + GPT-5.6 Sol

Exact solution publication status

Public

Publication date

2026-08-27

How this solution was produced

GPT-5.6 Sol operating through MathGraph's verifier-governed developmental loop, with repeated Lean compilation against the frozen LeanEval abel_ruffini workspace, residual diagnosis, targeted proof repair, and human direction/review. The final submission was independently checked by Lean in the pinned benchmark workspace and passed the exact Submission build, workspace test, and no-placeholder scan in MathGraph CI.

Acknowledgements

• I understand that the lean-eval CI will fetch my submission URL and run comparator on every lakefile.toml whose name matches a benchmark problem id.
• I understand that only the set of solved problem IDs, along with the metadata entered above, will be published to the public leaderboard results store.
• I understand that an encrypted copy of the submission source tree (compressed gzipped tar, ≤ 10 MiB) is retained indefinitely in the private leanprover/lean-eval-audit repository for audit purposes, decryptable only by the benchmark maintainers described in the audit policy.