Formal evidence
Independent review accepted the recorded build, exact declarations, unfinished-step scan, and axiom evidence.
Geometry · formal theorem
Heron’s Formula — Coordinate Identity
For any three points in ℝ², the square of twice their signed coordinate area equals four times the Heron radicand of their side lengths.
Scope: For any three points in ℝ², including collinear triples, the square of twice their signed coordinate area equals four times the Heron radicand of their side lengths.
Lean checkedBuild passed
Unfinished proof stepsNone
PublicationAccepted formal theorem
Exact formal proposition
Hypotheses and conclusion
This is the meaningful proposition proved by the checked wrapper declaration. It is extracted from the same commit-pinned Lean source.
noncomputable def HeronFormulaStatement : Prop :=
∀ p q r : Point,
(twiceSignedArea p q r) ^ 2 =
4 * heronRadicand (side q r) (side r p) (side p q)Definitions used in this proposition
Point
abbrev Point : Type :=
Fin 2 → ℝsqDist
def sqDist (p q : Point) : ℝ :=
(p 0 - q 0) ^ 2 + (p 1 - q 1) ^ 2side
noncomputable def side (p q : Point) : ℝ :=
Real.sqrt (sqDist p q)twiceSignedArea
def twiceSignedArea (p q r : Point) : ℝ :=
(q 0 - p 0) * (r 1 - p 1) - (q 1 - p 1) * (r 0 - p 0)heronRadicand
noncomputable def heronRadicand (a b c : ℝ) : ℝ :=
let s := (a + b + c) / 2
s * (s - a) * (s - b) * (s - c)Lean wrapper declaration
The checked endpoint names the proposition displayed above. This short declaration is useful for source identity, but the expanded proposition is the mathematical statement to read first.
theorem heronFormula :
HeronFormulaStatementThe theorem at a glance
Heron's coordinate identity at a glance
Accessible transcript
(2Aₛ)² = 4s(s − a)(s − b)(s − c)
The checked proof expands Heron's four factors, rewrites them through squared side lengths, and matches the resulting polynomial with the squared coordinate determinant. It establishes the squared twice-signed-area identity for any three planar points, not a separate unsigned square-root formula.
Read the complete poster transcript
PLANE GEOMETRY · COORDINATE IDENTITY
HERON’S FORMULA
COORDINATES AND SIDE LENGTHS MEASURE THE SAME AREA
FOR ANY p, q, r ∈ ℝ²
a = |q − r| · b = |r − p| · c = |p − q|
s = (a + b + c)/2
(2Aₛ)² = 4s(s − a)(s − b)(s − c)
Aₛ is the signed coordinate area.
Squaring removes the choice of orientation.
r = (x₃, y₃)
b = |r − p| · a = |q − r|
2Aₛ = |x₂ − x₁ y₂ − y₁; x₃ − x₁ y₃ − y₁|
O · p = (x₁, y₁) · c = |p − q| · q = (x₂, y₂)
HOW THE PROOF MOVES
1 · EXPAND HERON’S FOUR FACTORS
16s(s − a)(s − b)(s − c)
2 · REWRITE USING SIDE SQUARES
4a²b² − (a² + b² − c²)²
3 · USE THE COORDINATE DETERMINANT
4a²b² − (a² + b² − c²)² = 4(2Aₛ)²
4 · COMPARE THE IDENTITIES
(2Aₛ)² = 4s(s − a)(s − b)(s − c)
EXACT SCOPE
The squared twice-signed-area identity for three points in ℝ².
No nondegeneracy assumption. Not a separate proof of an unsigned square-root formula.
Theorem schematic
One area in two mathematical languages
(2Aₛ)² = 4s(s − a)(s − b)(s − c)
For any three points in ℝ², the square of twice their signed coordinate area equals four times s(s − a)(s − b)(s − c), where a, b, c are the side lengths and s is their semiperimeter. Squaring removes orientation and permits degenerate triples.
Result boundary
What this theorem does—and does not—establish
For any three points in ℝ², including collinear triples, the square of twice their signed coordinate area equals four times the Heron radicand of their side lengths.
- Because the identity is squared, it does not select an orientation or separately state a positive unsigned-area formula.
About these visual explanations
These AI-generated visuals explain the theorem and proof route; they are not proof evidence. Their publication review was completed separately from review of the formal result. The exact Lean proposition and checked source remain authoritative.
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.
Independent review
Review record
Independent review accepted
Lean checks the exact proof. Independent reviewers accepted evidence completeness, statement alignment, scope, and public wording; the visual review covers explanation only.
Statement alignment
The formal declaration was accepted against the named theorem and its exact variant.
Result boundary
The accepted boundary keeps nearby stronger or commonly confused claims out of scope.
Public wording
Independent review accepted the retained theorem explanation and source presentation. Generated media follows a separate review and promotion gate.
Canonical source
The first-party source link is pinned to the checked package commit and exact Lean file.
Accepted result
A validated accepted-result record binds the four reviews to the checked formalization.