ProofAtlas

Lean evidence record

Bondy's Minimum-Degree Longest-Cycle Conjecture: Lean evidence

This technical record binds the exact theorem statement to its commit-pinned Lean source, checker results, assumptions, and publication-review status.

Read theorem page
Lean buildpassed
Unfinished proof stepsNone
Publication reviewsPending

Exact recorded Lean statement

The declaration this evidence supports

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

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.

Technical evidence record

Source identity, checker results, and assumptions

Main Lean declaration
bondy_longest_cycle
Source commit
9e13b044d882

Mechanical evidence

Lean verification

These fields support the exact Lean declaration, not a broader informal claim.

Why ProofAtlas acceptance is still pending: the supplied release audit records a successful one-worker rehash build, no unfinished proof commands, and the reported axiom closure. It does not retain the complete command/output transcript and clean-source collection record required for accepted-result status.

Artifact ID
artifact.bondy.minimum-degree-longest-cycle-conjecture.lean-package.v001
Declarations covered by recorded evidence
Bondy.bondy_longest_cycle
Lean build
passed
Recorded build time
Not retained in the supplied release audit
Unfinished proof check
passed
Lean toolchain
leanprover/lean4:v4.30.0-rc2
Recorded source commit
9e13b044d8821b587935fa3019d913699eadffa2
Source SHA-256
sha256:39f30c64552384723952a7a5db99d1254ac0dc72658b71b71e6b75d0d59bf85a
Statement alignment
under review

Lean foundations

Standard foundations used by the proof

Lean reports the logical foundations below through Mathlib. They are standard proof-system foundations, not conjectural mathematical assumptions about this theorem. The recorded closure stays within the approved classical_mathlib_standard profile, with no unexpected axiom or unfinished-proof placeholder.

  • Classical.choice
  • Quot.sound
  • propext

Files and machine-readable evidence

Reproduce or inspect the recorded check

Use the complete first-party source bundle for reconstruction, or inspect the exact main file and checker evidence separately. Mathlib and other third-party dependencies are identified but not rebundled.

Complete checked Lean source · 204 Lean files · 1 evidence record · Download ZIPBrowse counted source onlineDownload main Lean fileDownload checker evidence (JSON)Download Apache-2.0 license

Review results

Publication review remains open

This exact artifact has not yet cleared every publication-review gate. The Lean evidence below remains useful for inspecting what was checked, but it is not an accepted result record.

Read the publication-review details

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.