The agent chooses the problem. CI chooses whether mathematics happened.
AlphaProof Nexus evolution on Erdős Problem #25 — does every congruence-avoiding set have a logarithmic density? Open problem, formalized in Lean 4.
A finite algebraic covering system for the Erdos-Straus conjecture, verified to 10^11 (max A = 359); exploratory search to 1.2x10^12 finds A = 479. Gateway decompositions via divisors of N^2.
FO4 constraint-isolation boundary module for Cayley/local-rigidity arguments; terminal Math-AI question preserved as OPEN_PROBLEM_REQUIRED.
Computational search for the [22,6,13]₄ linear code over GF(4) — a 25-year open problem in coding theory. Record excess E*=1. 441+ programs, 2.5B+ evaluations, 8 structural theorems including the Freedom Theorem, the Distance Theorem, and the Residual Reduction to [9,5,4]₄. Proyecto Estrella, Madrid.
Miura-ori origami flip graphs: candidate general diameter proof using convex order, majorization, and discrete Lipschitz functions, with reproducible verification.
Literature-first, reproducible Mathematics Commons workbench for the Erdős–Straus conjecture
The square achievement game on an n x n grid is a first-player win for every n >= 5. Solvers, logs and verification for the nine previously open cases n = 6..14.
Kernel-checked Lean 4 proof that no infinite simple paramedial quasigroups exist (Loops '03 open problem).
Binary Smallest Grammar Problem NP-completeness candidate proof - manuscript, verification code, reproducibility tests, and expert-audit materials.
A concise proof roadmap for the Kaser-Lemire half-degree irreducible-polynomial conjecture, with proved reductions and the remaining high-Witt obstruction.
To associate your repository with the open-problem topic, visit your repo's landing page and select "manage topics."