Lean evidence record
Brianchon’s Theorem: Lean evidence
This technical record binds the exact theorem statement to its commit-pinned Lean source, checker results, assumptions, and publication-review status.
Exact recorded Lean statement
The declaration this evidence supports
theorem brianchonTheorem : BrianchonTheoremStatementLine 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
brianchonTheorem- Source commit
3c957551a287
Mechanical evidence
Lean verification
These fields support the exact Lean declaration, not a broader informal claim.
- Artifact ID
artifact.known-brianchon-theorem.nonsingular.v001- Accepted-result title
- Accepted Result: Brianchon’s Theorem
- Accepted-result status
- Accepted formalization of a known theorem
- Accepted-result boundary
- For six recorded nonzero lines tangent to a nonsingular real projective conic, the three joins of opposite consecutive-line intersections are concurrent. The formal BrianchonGeneralPosition predicate requires each line to be represented by a nonzero coordinate triple (at least one coordinate is nonzero); it does not require the six tangent lines or their recorded vertices to be pairwise distinct. Non-claim: The superseded v0 tangency predicate was too weak and is formally refuted; only the repaired nonsingular-conic statement is claimed. Non-claim: This is a homogeneous-coordinate theorem over ℝ, not a synthetic-geometry or arbitrary-field formulation.
- Declarations covered by recorded evidence
AtlasKnownTheorems.BrianchonTheorem.brianchonTheoremAtlasKnownTheorems.BrianchonTheorem.BrianchonTheoremStatementAtlasKnownTheorems.BrianchonTheorem.brianchonTheoremStatement_v0_false- Lean build
- passed
- Recorded build time
- 4.4 s one machine-dependent evidence run, not a benchmark
- Evidence collected
- · clean-source provenance recorded
- Unfinished proof check
- passed
- Lean toolchain
leanprover/lean4:v4.29.1- Recorded source commit
3c957551a2879a961a6a05d15fffd66475e08cf5- Source SHA-256
sha256:6988a3e2e49a0dd66f159b6f0b51fd0acc8cc023c79b32d3673d1bc3db920d1f- Statement alignment
- accepted
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.choiceQuot.soundpropext
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.
Review results
Publication reviews accepted
All four required publication-review gates are accepted for the reviewed presentation of this exact theorem. The review results are separate from the Lean build and do not broaden the formal statement.
Read the publication-review details