ProofAtlas

ProofAtlas research case study

August 16, 2026 · Lech Mazur · developed with AI agents through ProofAtlas

Starting frontierBondy's 1980 open conjectureAI-developed Lean-checked candidateAugust 16 paper + audited 204-module Lean release
Evidence and status →

Graph theory · formal theorem

Bondy's Minimum-Degree Longest-Cycle Conjecture

The companion paper presents a candidate proof of Bondy's minimum-degree longest-cycle conjecture. Paper-to-formal-statement alignment is under review. Lean checks only the exact displayed endpoint Bondy.bondy_longest_cycle at the audited source commit; its 204-module first-party cone reports only standard classical foundations.

Scope: For every finite simple k-connected graph satisfying Bondy's natural-number minimum-degree inequality, every vertex-simple path disjoint from every longest cycle has order strictly below k.

Lean checkedRecorded build passed
Unfinished proof stepsNone
PublicationReview pending
Bondy longest-cycle statement mapA longest cycle in a sufficiently connected graph leaves no vertex-simple residual path of order k or more under Bondy's exact minimum-degree threshold.
Exact scope: For every finite simple k-connected graph satisfying Bondy's natural-number minimum-degree inequality, every vertex-simple path disjoint from every longest cycle has order strictly below k.

Exact formal proposition

Hypotheses and conclusion

theorem bondy_longest_cycle {V : Type u} [Fintype V] [DecidableEq V] (G : SimpleGraph V) (k : ℕ) (hk : 1 ≤ k) (hconn : VertexConnectedAtLeast G k) (hsource : Fintype.card V + k * (k - 1) ≤ (k + 1) * minimumDegree G) (C : VCycle G) (hC : IsLongestCycle G C) :
    ∀ P : VPath G, Disjoint P.support C.support → P.order < k

Result boundary

What this theorem does—and does not—establish

For every finite simple k-connected graph satisfying Bondy's natural-number minimum-degree inequality, every vertex-simple path disjoint from every longest cycle has order strictly below k.

Line counts exclude blank lines; comments and documentation count. The total is the commit-pinned first-party Lean import closure; Mathlib and other third-party dependencies are excluded.

Continue the mathematics

Open questions and extensions

The pinned theorem and its complete local import closure let people and AI agents inspect the proof, compare another route, isolate reusable lemmas, or formulate a stronger exact statement. Lean checks each proposed extension against its own exact statement.

What the source ZIP contains

The ZIP contains the checked first-party Lean import closure, exact statements and boundaries, license, notice, evidence, source-footprint manifest, and continuation data. Mathlib and other third-party dependencies are not bundled.

Complete checked Lean source · 204 Lean files · 1 evidence record · Download ZIPBrowse the checked source onlineDownload main Lean fileDownload checker evidence (JSON)Download Apache-2.0 license
Formal theorem review status — 4 questions open

Independent review

Four review questions remain open

Lean has checked the exact source, but ProofAtlas has not accepted this result. Independent AI, human, or mixed reviewers may examine the build evidence, statement alignment, result boundary, and public wording. Review does not replace Lean's check or broaden the theorem.

Review 1

Formal evidence

An independent reviewer must inspect the recorded build, declarations, unfinished-proof-step check, and disclosed foundations.

Review 2

Statement alignment

The formal declaration must be reviewed against the theorem wording and its exact variant.

Review 3

Result boundary

The limits must be checked so the page cannot imply a broader theorem.

Review 4

Public wording

The explanation, infographic labels, and source presentation need independent review.

Source

Canonical source

The permanent source link and downloadable files must be approved for public citation.

Final record

Accepted result

After the four reviews and source route are ready, an accepted-result record must bind them to this exact formalization.

Credit for this release

Contributors and roles

Authorship and other contributions are recorded separately for this version.

Authorship

Paper author
Lech Mazur

Contributions

  • Direct contributionOpenAI GPT-5.6 Pro

    OpenAI GPT-5.6 Pro has source-reported roles in mathematical exploration, proof development, computational testing, adversarial auditing, exposition, and AI-assisted formalization development.

    • Computation
    • Exposition
    • Formalization
    • Gap or error discovery
    • Proof strategy
  • Direct contributionLech Mazur

    Lech Mazur is the paper author and accountable editor and directed the AI-assisted research, verification process, output selection, and reconciliation.

    • Exposition
    • Proof strategy
    • Research direction

Citation

Cite this release

Use the version-specific citation so the authorship, scope, and public record remain attached.

Release history

Versions and public record

Release
Paper release
Version
revised public version of August 16, 2026
Published
Canonical page
Open canonical page
Earlier release
credit.release.bondy-longest-cycle-proof.v001

Release chronology

This version is part of the release history. No independent external timestamp is claimed.

Scope of this release

  • No independent external priority anchor or literature-completeness review is recorded.
  • ProofAtlas has not rerun the substantial Lean build for this page update or reproduced the proof in an unrelated implementation.
  • Specialist mathematical review and ProofAtlas accepted-result review remain open.
  • The release does not establish historical priority or verify every citation and expository statement in the companion paper.
  • The retained audit is pinned to source commit 9e13b044d8821b587935fa3019d913699eadffa2 and does not cover the later local commit 9a6d94363495d2578fed87911e5a247af3ce3394.