CITATION.cff

cff-version: 1.2.0
message: "If you use this repository, please cite it as below."
title: "Euclids-path: a machine-verified formalization of the perpetual-engine programme (Lean 4)"
abstract: >-
  A Lean 4 formalization organised around a single physical prohibition — the
  impossibility of a perpetual engine (Fermat's infinite descent for the centres
  of the Euclidean pairs 6m±1) — reducing the twin-prime conjecture to a single
  open node accepted from outside by one quarantined axiom (the "first cause"),
  and reading the great conjectures as shadows of the same prohibition. Honesty is
  machine-checked: exactly one non-standard axiom, exactly one `sorry`, an
  axiom-taint count re-verified on every run. No Millennium problem is claimed solved.
type: software
authors:
  - family-names: Semenov
    given-names: "D. S."
    affiliation: "Independent researcher"
    orcid: "https://orcid.org/0009-0006-6213-0638"
  - family-names: Galieva
    given-names: "L. R."
    affiliation: "Independent researcher"
    orcid: "https://orcid.org/0009-0009-8656-6040"
repository-code: "https://github.com/elamaunt/Euclids-path"
url: "https://elamaunt.github.io/Euclids-path/"
license: Apache-2.0
date-released: "2026-07-04"
keywords:
  - twin primes
  - infinite descent
  - formalization
  - Lean 4
  - first cause
  - Riemann hypothesis
  - Navier-Stokes
  - Collatz
doi: "10.5281/zenodo.21198730"
identifiers:
  - type: doi
    value: "10.5281/zenodo.21198730"
    description: "Zenodo concept DOI (all versions; resolves to the latest release)"