← Research sourcesCuration review · 2026-10-11What did public discussion reveal?
Eleven missing contributions added, one comparison corrected, and nine existing decisions retained.
Targeted audit of 21 contributions prompted by public discussion, against the 98-record local catalog. This is not a complete survey of all pending research.
Comments are discovery leads and attributed opinions. Inclusion and ratings use exact source statements, baselines and attribution; votes are not evidence and no full proof audit was performed.
Formalization of known mathematics can qualify; a registry flag alone does not establish a reason to exclude it. Attribution is checked in the full source when the abstract does not explain the AI role.
Discussion compared with our decisions
OpenAI reports: Navier–Stokes blowup with smooth forcing
AddedImportance: majorBefore: Awaiting detailed review; absent from curated progress.
Public discussion: Discussion includes excitement about the regularity frontier and objections concerning forcing, physical applicability, and credit. None justifies silently omitting the stated theorem.
Our assessment: If correct, settles the specified smooth-forcing breakdown alternatives of a Millennium Prize problem, despite leaving the unforced question separate.
Scope and limits: This is a forced result; unforced global regularity and real-world fluid prediction are separate questions. Clay’s 11 September announcement describes an apparent settlement, not a completed proof audit or prize award. AIProofWatch has not compiled the Lean project or checked the full proof. Priority and data-use disagreements are not adjudicated here.
Read the curated contribution →
Source evidence and discussion links
OpenAI reports: smooth unforced Euler blowup on R³
AddedImportance: majorBefore: Awaiting detailed review; absent from curated progress.
Public discussion: Public fluid-equation discussion emphasizes the forcing distinction and earlier human methods; the unforced statement merits its own record.
Our assessment: If correct, resolves the smooth whole-space unforced Euler finite-time breakdown target, beyond forced or lower-regularity variants.
Scope and limits: Euler has no viscosity and this statement does not establish unforced Navier–Stokes blowup. The earlier forced Euler work is distinct. AIProofWatch has not audited the proof or compiled the Lean artifact.
Read the curated contribution →
Source evidence and discussion links
Alpöge–Buckmaster: Boussinesq blowup with smooth forcing
AddedImportance: majorBefore: Awaiting detailed review; absent from curated progress.
Public discussion: Tao describes a methodological breakthrough while stressing understanding, unfinished exposition and inherited ideas. Omitting the human-led AI-assisted precursor loses important attribution.
Our assessment: If correct, establishes smooth-forcing breakdown for a central fluid-equation model and extends a method discussed as a route toward other regularity problems.
Scope and limits: Forcing is essential to this statement. Tao’s explanation is an assessment of the ideas, not a complete independent proof check. The current manuscript was simplified after its first release; AIProofWatch reviewed its stated target and AI disclosure, not the full proof.
Read the curated contribution →
Source evidence and discussion links
AI-assisted counterexample to Grothendieck’s group-scheme question
AddedImportance: majorBefore: Awaiting detailed review; absent from curated progress.
Public discussion: Buzzard finds this algebraic example especially interesting; another expert reportedly questions its difficulty. Ease and publicity do not undo the stated counterexample.
Our assessment: If correct, refutes a longstanding general group-scheme assertion with an explicit order-four example, retaining the known positive cases.
Scope and limits: This does not contradict the commutative or reduced-base theorems. Buzzard reports compiling and checking a version in July; this is attributed checking, not a AIProofWatch rerun or an audit of every later revision.
Read the curated contribution →
Source evidence and discussion links
AlphaDev: faster small sorting routines in LLVM libc++
AddedImportance: notableBefore: Awaiting detailed review; absent from curated progress.
Public discussion: Comments distinguish useful library improvements from new asymptotic sorting theory. The concrete adoption supports inclusion, with a notable rating and hardware caveats.
Our assessment: A deployed improvement to a widely used algorithmic primitive has substantive reach despite being a constant-factor optimization.
Scope and limits: Speedups depend on implementation, processor and data. This does not beat the comparison-sorting asymptotic lower bound. Later human routines can outperform particular AlphaDev kernels. AIProofWatch has not rerun the benchmarks.
Read the curated contribution →
Source evidence and discussion links
AlphaEvolve-assisted large hypercubes in Bruhat order
AddedImportance: notableBefore: Awaiting detailed review; absent from curated progress.
Public discussion: An author’s public explanation stresses a new conceptual connection and human-written proofs. The general theorem qualifies beyond the finite search that suggested it.
Our assessment: If correct, improves a linear construction scale to n log n and connects Bruhat order with low-discrepancy permutations and representation-theoretic applications.
Scope and limits: The displayed exact construction is for powers of two and does not determine every exact maximum. Humans identified, generalized and proved the pattern; this is not an autonomous AI proof. AIProofWatch has not audited the argument.
Read the curated contribution →
Source evidence and discussion links
Gauss: AI-assisted strong prime number theorem formalization
AddedImportance: notableBefore: Awaiting detailed review; absent from curated progress.
Public discussion: Discussion treats completion of this research formalization as substantive. The known theorem does not justify excluding the new formalization.
Our assessment: A substantial formal development and reusable analytic infrastructure merit inclusion even though the underlying mathematical theorem is known.
Scope and limits: This is formalization of established mathematics, not a new prime-distribution theorem. The repository identifies reused files and human scaffolding. AIProofWatch has not compiled or audited its statements and axioms.
Read the curated contribution →
Source evidence and discussion links
OpenAI reports: a counterexample to Hadwiger’s conjecture
AddedImportance: majorBefore: Awaiting detailed review; absent from curated progress.
Public discussion: Commenters explicitly singled out this target as important. Primary-statement review confirms it is distinct from the statements already curated.
Our assessment: If correct, disproves a central graph-minor/coloring conjecture and its stated fractional weakening.
Scope and limits: This is a preprint claim about graph coloring and minors, separate from the plane-coloring problem. AIProofWatch reviewed the stated theorem and baseline, not the proof or a formal checker.
Read the curated contribution →
Source evidence and discussion links
OpenAI reports: Mahler’s conjecture for general convex bodies
AddedImportance: majorBefore: Awaiting detailed review; absent from curated progress.
Public discussion: Commenters explicitly singled out this target as important. Primary-statement review confirms it is distinct from the statements already curated.
Our assessment: If correct, determines the exact minimum and equality cases for unrestricted convex bodies in every dimension.
Scope and limits: The general and symmetric Mahler statements are distinct even though the manuscripts share a source family. AIProofWatch has not audited this proof or run a formal checker.
Read the curated contribution →
Source evidence and discussion links
OpenAI reports: a power saving for exact discrete Fourier transforms
AddedImportance: majorBefore: Awaiting detailed review; absent from curated progress.
Public discussion: Commenters specifically highlight the sub-n log n transform despite its extremely small exponent saving. The exact theorem supports significance with explicit model restrictions.
Our assessment: If correct, breaks the n log n arithmetic-operation scale for all transform lengths in the stated model; the small saving and practical limitations do not erase its theoretical impact.
Scope and limits: Unit-cost exact complex arithmetic, unrestricted coefficient magnitudes, O(log n)-bit indexing and one specified Fourier root are assumed. This is not a bit-complexity or numerical-stability theorem and does not contradict bounded-coefficient or well-conditioned lower bounds. The tiny exponent saving gives no practical-speedup guarantee. AIProofWatch has not audited the proof.
Read the curated contribution →
Source evidence and discussion links
AlphaEvolve: 48 multiplications for 4×4 complex matrices
Scope correctedImportance: notableBefore: Notable; comparison model underspecified.
Public discussion: A critic cites Waksman’s smaller count; a paper author responds that commutative products do not yield the same tensor decomposition.
Our assessment: The criticism warrants a precise model correction, not deletion or an importance promotion.
Scope and limits: This does not establish a new asymptotic exponent or universal hardware speedup. It is not the same field as AlphaTensor’s F₂ result. AIProofWatch has not checked the decomposition. The novelty comparison concerns bilinear tensor rank, not the fewest products in every commutative arithmetic model. Waksman-type algorithms cannot be substituted as tensor-rank baselines.
Read the curated contribution →
Source evidence and discussion links
OpenAI reports: Zero-free regions for zeta and L-functions
RetainedImportance: majorBefore: Major; already curated.
Public discussion: Readers single out quasi-Riemann as a major advance while noting that full RH is separate.
Our assessment: If correct, establishes a uniform zero-free half-plane and resolves the quasi-Riemann question. It does not resolve the full Riemann hypothesis.
Scope and limits: This is the quasi-Riemann hypothesis, not the full Riemann hypothesis. The principal pole at 1 is allowed. Preprint. AIProofWatch reviewed the source statement and scope, not the full proof, and has not independently run a formal checker.
Read the curated contribution →
Source evidence and discussion links
OpenAI reports: Hilbert’s tenth problem over the rationals
RetainedImportance: majorBefore: Major; already curated.
Public discussion: Readers identify Hilbert’s tenth problem over Q as a major target.
Our assessment: If correct, resolves the rational version of a recognized undecidability problem, beyond the established integer case.
Scope and limits: This is a rational-solvability decision problem with variable dimension. It does not rule out decision algorithms for particular restricted polynomial classes. Preprint. This is a source-statement and significance assessment, not a proof audit. No independent checking or successful formal compilation is asserted by this entry.
Read the curated contribution →
Source evidence and discussion links
OpenAI reports: The Unique Games Conjecture
RetainedImportance: majorBefore: Major; already curated.
Public discussion: Readers emphasize Unique Games and approximation complexity; it does not settle P versus NP.
Our assessment: If correct, establishes the full stated Unique Games hardness target underlying many approximation thresholds.
Scope and limits: The alphabet and reduction constants depend on the fixed errors. NP-hardness does not prove P≠NP, and companion approximation consequences are not separate discoveries in this record. Preprint. This is a source-statement and significance assessment, not a proof audit. No independent checking or successful formal compilation is asserted by this entry.
Read the curated contribution →
Source evidence and discussion links
OpenAI reports: The symmetric Mahler conjecture
RetainedImportance: majorBefore: Major; already curated.
Public discussion: Readers emphasize both Mahler conjectures; the symmetric entry already covers its sharper restricted target.
Our assessment: If correct, determines the stated all-dimensional symmetric minimum and its equality cases.
Scope and limits: Origin symmetry is essential to this statement. The general nonsymmetric Mahler manuscript and the symplectic companion are distinct claims, not counted again in this entry. Preprint. This is a source-statement and significance assessment, not a proof audit. No independent checking or successful formal compilation is asserted by this entry.
Read the curated contribution →
Source evidence and discussion links
OpenAI reports: Kaplansky zero-divisor counterexamples
RetainedImportance: majorBefore: Major; already curated.
Public discussion: Readers emphasize Kaplansky counterexamples and the structural consequences.
Our assessment: If correct, refutes the stated zero-divisor conjecture while retaining torsion-freeness and finite presentation.
Scope and limits: The construction is in characteristic two. It does not establish a counterexample over every field, and it is distinct from the separate direct-finiteness claim. Preprint. This is a source-statement and significance assessment, not a proof audit. No independent checking or successful formal compilation is asserted by this entry.
Read the curated contribution →
Source evidence and discussion links
OpenAI reports: A torsion-free direct-finiteness counterexample
RetainedImportance: majorBefore: Major; already curated.
Public discussion: Readers emphasize direct finiteness; retain its positive-characteristic scope.
Our assessment: If correct, refutes the stated positive-characteristic direct-finiteness target even for a torsion-free finitely presented group.
Scope and limits: This entry covers the torsion-free two-element-field construction. Other characteristic, determinant, or cellular-automaton companions are not separate records here. Preprint. This is a source-statement and significance assessment, not a proof audit. No independent checking or successful formal compilation is asserted by this entry.
Read the curated contribution →
Source evidence and discussion links
OpenAI reports: The free group factor isomorphism problem
RetainedImportance: majorBefore: Major; already curated.
Public discussion: Readers emphasize the free group factor isomorphism target.
Our assessment: A claimed general advance on a longstanding structural problem; importance assumes the scoped statement is correct.
Scope and limits: The claim is a trace-preserving normal *-isomorphism of the specified factors. It concerns von Neumann algebras, not an isomorphism of the underlying free groups. Preprint. AIProofWatch read the source statement and context; it has not refereed the proof, compiled a formal development, or established community acceptance.
Read the curated contribution →
Source evidence and discussion links
OpenAI reports: Global classical relativistic Vlasov–Maxwell solutions
RetainedImportance: majorBefore: Major; already curated.
Public discussion: A commenter describes major Vlasov–Maxwell implications but says the exposition is difficult to understand; that is not a proof check.
Our assessment: A claimed general advance on a longstanding structural problem; importance assumes the scoped statement is correct.
Scope and limits: One species with no background charge is the stated model. Initial particle density is nonnegative, smooth and compactly supported; fields have finite energy, bounded derivatives, and satisfy the Gauss constraints. This does not resolve Navier–Stokes regularity. Preprint. AIProofWatch read the source statement and context; it has not refereed the proof, compiled a formal development, or established community acceptance.
Read the curated contribution →
Source evidence and discussion links
Erdős #728: an AI-assisted factorial-divisibility proof and human writeup
RetainedImportance: notableBefore: Notable; already curated.
Public discussion: Comments celebrate an AI milestone but question autonomy and earlier literature. Mathematical scope remains a focused factorial-divisibility result.
Our assessment: A scoped result on a named research problem, with prior literature and human contributions retained.
Scope and limits: Related literature and subsequent refinements affect novelty and attribution. This is not a claim of sole AI priority. AIProofWatch has not compiled the original formal development.
Read the curated contribution →
Source evidence and discussion links
AI-assisted small counterexamples to the Gaussian Moments Conjecture
AddedImportance: majorBefore: Awaiting detailed review; absent from curated progress.
Public discussion: The counterexample discussion and registry led to this candidate. The abstract alone did not establish its AI role; the full paper’s explicit AI-provenance section resolves that uncertainty.
Our assessment: If correct, refutes the Gaussian Moments Conjecture with small explicit witnesses, beyond a nonconstructive implication in a much larger dimension.
Scope and limits: Complex coefficients are essential. Dimension two remains unsettled, and dimension one was already established. These examples were not derived from the coordinates of the Jacobian counterexample. The manuscript’s algebraic checks by Claude are not independent human verification. AIProofWatch reviewed the theorem, comparison and full-text AI disclosure, not the complete proof.
Read the curated contribution →
Source evidence and discussion links
Browse the remaining screening decisions · Suggest another contribution
