∑ Math Proof Playground › Research › A387471

OEIS A387471

A formula for a geometric concurrence-counting sequence, with a complete proof manuscript and a substantial—but not complete—Lean formalization.

Mathematical proof candidateLean reductions greenExact statement not fully formalized

Claimed formula

a(n) = 6n − 5 when 5 ∤ n a(n) = 6n + 7 when 5 ∣ n

The paper argument uses trigonometric Ceva to convert the geometric concurrence condition into a three-sine relation, then into a weight-six vanishing sum of roots of unity. The published classification of minimal vanishing sums isolates ordinary families and an exceptional (R5:R3) family.

Mathematical proof architecture

  1. Apply trigonometric Ceva to encode concurrence.
  2. Use product-to-sum identities to reduce the condition to a six-root vanishing relation.
  3. Invoke the published weight-six classification of minimal vanishing sums of roots of unity.
  4. Reconstruct the integer index lattice for the ordinary families.
  5. Analyze the exceptional fifth-root family and derive the divisibility condition 5 ∣ n.
  6. Count the ordinary and exceptional solutions to obtain the two-case formula.

What Lean currently verifies

ComponentStatus
Exact product-to-sum identityKernel checked
Concurrence equation ↔ reduced three-sine equationKernel checked
Integer lattice reconstructionKernel checked
Ordinary and exceptional index familiesKernel checked
Two exceptional fifth-root sine identitiesKernel checked
5 ∣ n consequence for exceptional triplesKernel checked
Final arithmetic formula from classified familiesKernel checked
Grid-level six-root classification → index classificationKernel checked

GitHub Actions run 29433407515 passed. The source guard scans all Lean modules under proofs/lean/A387471 and rejects sorry, admit, native_decide, and sorryAx.

What remains

  1. Formalize the published weight-six vanishing-sum classification in Lean/Mathlib, or import a trusted formal version.
  2. Package the classified families as the exact finite solution set.
  3. Prove the final cardinality equality for the original exact sequence definition.
The draft PR intentionally does not inhabit ExactStatement. Therefore the full OEIS formula must not yet be described as completely Lean verified.

Current repository status

CRL draft PR #1 — Formalize the A387471 reduction in Lean

The proof manuscript can be publication-ready before the complete Lean formalization, but it still needs expert review of the roots-of-unity classification application and the exceptional-family counting.

← Research dashboard · OEIS A387471