AI Assisted
Mathematical Proofs

The sequence may contain several conjectures; this entry refers only to the statement in the linked artifact. Its correspondence to the OEIS text has not been audited.

The sequence may contain several conjectures; this entry refers only to the statement in the linked artifact. Its correspondence to the OEIS text has not been audited.

The sequence may contain several conjectures; this entry refers only to the statement in the linked artifact. Its correspondence to the OEIS text has not been audited.

The sequence may contain several conjectures; this entry refers only to the statement in the linked artifact. Its correspondence to the OEIS text has not been audited.

The sequence may contain several conjectures; this entry refers only to the statement in the linked artifact. Its correspondence to the OEIS text has not been audited.

The sequence may contain several conjectures; this entry refers only to the statement in the linked artifact. Its correspondence to the OEIS text has not been audited.

Existing literature already contains a solution.

Verification details are reported in the sources; proof artifacts have not been rebuilt for this catalogue.

Existing literature already contains a solution.

Reported by OpenAI; peer review and local proof rebuild are not recorded.

Reported by OpenAI; peer review and local proof rebuild are not recorded.

The sequence may contain several conjectures; this entry refers only to the statement in the linked artifact. Its correspondence to the OEIS text has not been audited.

The sequence may contain several conjectures; this entry refers only to the statement in the linked artifact. Its correspondence to the OEIS text has not been audited.

Reported by OpenAI; peer review and local proof rebuild are not recorded.

Reported by OpenAI; peer review and local proof rebuild are not recorded.

Formal coverage is reported as partial, and the bundled audits are not independent replication.

The unrefereed preprint has no formalization or independent check, and the disclosure credits the AI agent with the initial counterexample rather than every part of the final proof.

This is a formalization of an existing theorem, not a new prime-gap bound. The public flagship Lean theorem assumes Bombieri–Vinogradov as a hypothesis because that theorem is not yet in Mathlib.

The sequence may contain several conjectures; this entry refers only to the statement in the linked artifact. Its correspondence to the OEIS text has not been audited.

The preprint is disputed. A public technical objection alleges an inconsistent recurrence factor that invalidates the zero count used for the degree bound; the only whole-proof verification claimed in the paper is another language-model reading.

The sequence may contain several conjectures; this entry refers only to the statement in the linked artifact. Its correspondence to the OEIS text has not been audited.

This episode is not a disproof of Collatz. A kernel implementation bug invalidated the certificate; checker versions matter.

Existing literature already contains a solution.

This is an unreviewed claim in a problem with many failed proofs. The manuscript explicitly conflicts with a published corrigendum, contains no AI disclosure itself, and the AI attribution is only from a public author statement.

The original notes report a novelty and attribution dispute, rather than an allegation that the proof is wrong. See the linked coverage.

The sequence may contain several conjectures; this entry refers only to the statement in the linked artifact. Its correspondence to the OEIS text has not been audited.

The sequence may contain several conjectures; this entry refers only to the statement in the linked artifact. Its correspondence to the OEIS text has not been audited.

The sequence may contain several conjectures; this entry refers only to the statement in the linked artifact. Its correspondence to the OEIS text has not been audited.

The sequence may contain several conjectures; this entry refers only to the statement in the linked artifact. Its correspondence to the OEIS text has not been audited.

A formal variant may be weaker than the full numbered question. No local rebuild was performed.

Verification details are reported in the sources; proof artifacts have not been rebuilt for this catalogue.

The four-page preprint is unrefereed, has no formal artifact, and records author verification but no independent check.

A formal variant may be weaker than the full numbered question. No local rebuild was performed.

A formal variant may be weaker than the full numbered question. No local rebuild was performed.

The sequence may contain several conjectures; this entry refers only to the statement in the linked artifact. Its correspondence to the OEIS text has not been audited.

The preprint is unrefereed, unformalized and has no independent check recorded.

Existing literature already contains a solution.

Source-reported resolution; no formal artifact is listed.

Only part of this question is reported resolved.

The sequence may contain several conjectures; this entry refers only to the statement in the linked artifact. Its correspondence to the OEIS text has not been audited.

Verification details are reported in the sources; proof artifacts have not been rebuilt for this catalogue.

The sequence may contain several conjectures; this entry refers only to the statement in the linked artifact. Its correspondence to the OEIS text has not been audited.

Kernel acceptance checks the formal statement; correspondence with the intended problem must be checked separately.

Reported by OpenAI; peer review and local proof rebuild are not recorded.

Existing literature already contains a solution.

Human authors developed the proofs; the AI contribution was a method suggestion.

The precise density hypothesis and bound are in Theorem 1.6.

Reported by OpenAI; peer review and local proof rebuild are not recorded.

This is a reproof, not a first solution; Lichtman proved the conjecture earlier.

Reported by OpenAI; peer review and local proof rebuild are not recorded.

Reported by OpenAI; peer review and local proof rebuild are not recorded.

Verification details are reported in the sources; proof artifacts have not been rebuilt for this catalogue.

This is a source-reported AI reproof following a human disproof, not a claim of first discovery. The domain is the real numbers. The reported seven successes out of eight trials were not independently graded here.

The compared Lean theorem uses at least (k-1)n/2 + 1 edges. When (k-1)n is odd this is one edge stronger than the sharp classical hypothesis, so it is a marginally weaker result than the full conjecture.

The sequence may contain several conjectures; this entry refers only to the statement in the linked artifact. Its correspondence to the OEIS text has not been audited.

The sequence may contain several conjectures; this entry refers only to the statement in the linked artifact. Its correspondence to the OEIS text has not been audited.

The original notes report a novelty and attribution dispute, rather than an allegation that the proof is wrong. See the linked coverage.

An independent human proof is reported a day earlier; track discovery priority separately from formal verification.

The paper covers slack δ ≥ 1; the linked Lean coverage is reported as δ = 1 only. Do not label the whole theorem Lean-verified without an audit.

This is an AI-produced formalization of existing mathematics, not a new proof strategy or a new theorem. It builds on the Imperial College FLT project, flt-regular and Mathlib, and reproducing the independent checks requires substantial compute.

Existing literature already contains a solution.

The field matters: the 47-multiplication result is over F₂; the later characteristic-zero construction is a different claim. Neither establishes optimality.

The sequence may contain several conjectures; this entry refers only to the statement in the linked artifact. Its correspondence to the OEIS text has not been audited.

This very recent preprint is unrefereed and has not yet received broad specialist review. Its smooth, unforced result is distinct from earlier lower-regularity blowup constructions and from the concurrent forced-Euler work of Alpöge and Buckmaster. The public Lean project reports a full formalization, but its review status is self-assessed and the build has not been reproduced for this catalogue.

This settles only the (4,6) case, with an enormous explicit threshold. The preprint is unrefereed, unformalized and has no independent check.

Existing literature already contains a solution.

Disclose the dataset version and access conditions; neither a score change nor data access alone proves training contamination.

Compare the same assumptions and objective guarantee before calling a numerical bound an improvement.

A formal variant may be weaker than the full numbered question. No local rebuild was performed.

The linked Lean artifact covers the odd case; later even-case claims need separate evidence.

The authors report checking the arguments and references themselves. This entry does not assert external peer review or machine verification.

Verification details are reported in the sources; proof artifacts have not been rebuilt for this catalogue.

The short preprint is unrefereed, unformalized and has no independent check; the AI disclosure does not assign individual proof steps.

The preprint is unrefereed, unformalized and has no independent check recorded.

Most reported work used classical automated theorem provers. The finite-magma question is separate from the main implication graph.

This is an improvement to the record bound associated with Erdős

The sequence may contain several conjectures; this entry refers only to the statement in the linked artifact. Its correspondence to the OEIS text has not been audited.

Source-reported resolution; no formal artifact is listed.

Verification details are reported in the sources; proof artifacts have not been rebuilt for this catalogue.

A formal variant may be weaker than the full numbered question. No local rebuild was performed.

The notes report a higher-dimensional counterexample; the two-dimensional question is separate.

Neural networks identified relevant invariants; human mathematicians formulated and proved the theorem. An initial stronger conjecture had counterexamples. No formal proof artifact is listed.

Lean coverage is reported; no local rebuild was performed.

The notes report native_decide use in this artifact.

Lean coverage is reported; no local rebuild was performed.

Lean coverage is reported; no local rebuild was performed.

The notes report native_decide use in this artifact.

Lean coverage is reported; no local rebuild was performed. Rundström reportedly found an independent solution concurrently.

The Lean artifact reportedly covers existence of counterexamples at every base size, but not all additional base-two families or diameter computations; no third party audited statement-to-paper fidelity.

The notes report native_decide use in this artifact.

Lean coverage is reported; no local rebuild was performed.

Lean checks a counterexample to the matrix formulation. The classical implication from that formulation to Köthe's original statement is described but is not part of the formal development, and no independent ring-theory review is recorded.

A larger explicit construction gives a lower bound; it does not determine the maximum cap-set size.

The counterexample concerns five bits at p = 0.40 in the paper’s parameterization. It does not rule out majority optimality in other regimes. Human checking is described by the authors; no formal artifact is listed.

The counterexamples do not settle the corresponding question for the Landau equation. The preprint is unrefereed, unformalized and lacks an independent check.

The preprint is unrefereed and unformalized. The authors checked and reworked the proof, but no independent review is recorded.

The sequence may contain several conjectures; this entry refers only to the statement in the linked artifact. Its correspondence to the OEIS text has not been audited.

This is a same-day release, not yet peer reviewed or broadly accepted by specialists. The construction uses smooth external forcing, exactly as allowed by alternatives C and D of the official Millennium Prize formulation; it does not establish unforced blowup. OpenAI does not intend to claim the prize. The public Lean project reports full, sorry-free coverage, but its review status is self-assessed and the build has not been reproduced for this catalogue.

The preprint is unrefereed, unformalized and has no independent check recorded.

The sequence may contain several conjectures; this entry refers only to the statement in the linked artifact. Its correspondence to the OEIS text has not been audited.

Human reading only; no formalization is listed.

The sequence may contain several conjectures; this entry refers only to the statement in the linked artifact. Its correspondence to the OEIS text has not been audited.

The sequence may contain several conjectures; this entry refers only to the statement in the linked artifact. Its correspondence to the OEIS text has not been audited.

The sequence may contain several conjectures; this entry refers only to the statement in the linked artifact. Its correspondence to the OEIS text has not been audited.

The sequence may contain several conjectures; this entry refers only to the statement in the linked artifact. Its correspondence to the OEIS text has not been audited.

A disputed argument is not an accepted resolution. Keep the original claim, critique and response together.

An independent audit found a polarity error in a printed greedy-conditioning lemma and supplied a local repair. The correction does not independently verify the later sampleability, alignment, rounding or main parallel-repetition arguments; the Lean artifact was not rebuilt here.

Only a key combinatorial identity is reported as formalized; the geometric reduction requires separate checking.

The sequence may contain several conjectures; this entry refers only to the statement in the linked artifact. Its correspondence to the OEIS text has not been audited.

The sequence may contain several conjectures; this entry refers only to the statement in the linked artifact. Its correspondence to the OEIS text has not been audited.

Only part of this question is reported resolved.

A formal variant may be weaker than the full numbered question. No local rebuild was performed.

Only part of this question is reported resolved.

The notes describe conditional Lean developments with unformalized classical inputs, not unconditional certificates.

Human reading only; no formalization is listed.

The sequence may contain several conjectures; this entry refers only to the statement in the linked artifact. Its correspondence to the OEIS text has not been audited.

A positive proportion on the critical line is not a proof of the Riemann hypothesis.

The result is relative to a quantum oracle and does not separate QMA(2) from QMA in the unrelativized setting. The preprint is not formally verified or independently reviewed.

The sequence may contain several conjectures; this entry refers only to the statement in the linked artifact. Its correspondence to the OEIS text has not been audited.

The sequence may contain several conjectures; this entry refers only to the statement in the linked artifact. Its correspondence to the OEIS text has not been audited.

The linked Lean development is reported to check a seed identity, not the complete theorem.

Verification details are reported in the sources; proof artifacts have not been rebuilt for this catalogue.

The reported bound is Var(|X|²) ≤ 8n under the stated isotropy and log-concavity assumptions. AI worked from human-supplied prompts and mathematical context. No formal artifact is listed.

Verification details are reported in the sources; proof artifacts have not been rebuilt for this catalogue.

The sequence may contain several conjectures; this entry refers only to the statement in the linked artifact. Its correspondence to the OEIS text has not been audited.

The sequence may contain several conjectures; this entry refers only to the statement in the linked artifact. Its correspondence to the OEIS text has not been audited.

The sequence may contain several conjectures; this entry refers only to the statement in the linked artifact. Its correspondence to the OEIS text has not been audited.

This is a preliminary, unrefereed preprint without formalization or independent review.

Existing literature already contains a solution.

Formalization of an existing human theorem is distinct from discovering a new packing theorem. The preprint and repository have different reported scopes.

A formal variant may be weaker than the full numbered question. No local rebuild was performed.

A formal variant may be weaker than the full numbered question. No local rebuild was performed.

The sequence may contain several conjectures; this entry refers only to the statement in the linked artifact. Its correspondence to the OEIS text has not been audited.

A formal variant may be weaker than the full numbered question. No local rebuild was performed.

The sequence may contain several conjectures; this entry refers only to the statement in the linked artifact. Its correspondence to the OEIS text has not been audited.

The preprint is unrefereed and unformalized, with no independent check recorded. The authors supplied the known structural constraints and wrote the proofs and manuscript.

Human reading only; no formalization is listed.

The notes report formal coverage of the upper bound; the lower-bound construction is a separate obligation.

Human reading only; no formalization is listed.

Verification details are reported in the sources; proof artifacts have not been rebuilt for this catalogue.

The sequence may contain several conjectures; this entry refers only to the statement in the linked artifact. Its correspondence to the OEIS text has not been audited.

The result settles this natural function, not the general Boyar–Find question. The Lean statements have not received a recorded third-party semantic audit.

Reported by OpenAI; peer review and local proof rebuild are not recorded.

The claimed Lean development survives at a pinned commit rather than the repository's main branch. It proves a gluing conjecture reported to imply the percolation result; statement fidelity and the implication have not been independently audited here.

Human reading only; no formalization is listed.

Lab assessments and organiser assessments differ. Preserve both alongside the exact attempt and grading protocol.

Verification details are reported in the sources; proof artifacts have not been rebuilt for this catalogue.

These are multiple attempts at one problem set. Scores, time limits, grading and formal coverage are not interchangeable.

Public formal code does not by itself establish that its statements match the original competition problems.

Verification details are reported in the sources; proof artifacts have not been rebuilt for this catalogue.

Historical computer assistance and later formalization; not a modern machine-learning discovery.

Historical computer-assisted proof and formalization; not evidence of a new AI-discovered theorem.

Classical automated deduction predates modern LLMs; keep its role explicit.