ApplePie

"If you wish to make an apple pie from scratch, you must first invent the universe." — Carl Sagan

A Lean 4 project that formalizes physics with types and an explicit epistemic-status layer.

The premise: physics papers are written in prose, and prose hides things. When you compile a physical claim into a type system, you have to decide whether it's a theorem, a postulate, an empirical fact, a hypothesis, or a flat-out guess — and the type system won't let you cheat.

So that's what's happening here. SR, the Standard Model, cosmology — all gradually getting reduced to Lean terms with Status tags that mean what they say. When something turns out to be wrong (and it does — see the 2HDM case study), the framework catches it.

It is an ambitious goal. The discipline below is what keeps the attempt auditable rather than merely aspirational.

The five tags

A new physical claim falls into one of:

• .theorem proof — proved in Lean. The constructor takes the proof as an argument, so the kernel rejects anything without a real proof.
• .postulate "rationale" — adopted by convention. Explain why.
• .empirical [sources] — known from experiment. Primary citation required.
• .hypothesis "rationale" — currently under test. Explain falsifiability.
• .speculation "notes" — not yet operationalized.

Tags don't compete; they describe why something is in the library. A result with a Lean proof is a theorem regardless of whether you could also tag it empirical.

What it looks like in practice

-- Lorentz transformations are closed under multiplication.
-- The .theorem constructor takes a proof of the claimed proposition;
-- if `IsLorentz.mul` didn't actually prove it, this wouldn't compile.
instance : Claim (∀ M N : Matrix (Fin 4) (Fin 4) ℝ,
    IsLorentz M → IsLorentz N → IsLorentz (M * N)) :=
  ⟨.theorem (fun _ _ hM hN => IsLorentz.mul hM hN)⟩

-- The 1887 Michelson–Morley null result is an empirical anchor,
-- not something we prove. Source citation is required.
def principleOfRelativity : Status :=
  .empirical [Sources.MichelsonMorley1887]

Quick start

# install Lean
curl -sSf https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \
  | sh -s -- -y --default-toolchain none
export PATH="$HOME/.elan/bin:$PATH"

# build (~10 min cold, ~30s warm) and run the soundness checks
lake exe cache get
lake build
bash scripts/audit.sh

If everything is green: thousands of build jobs of Lean 4 + mathlib + Physlib + ApplePie are sitting on your machine, and the audit script confirms there's no sorry and no fake theorems hiding anywhere.

Findings

ApplePie tracks contributions — claims that advance the upstream formalization state of physics, classified by magnitude:

• closure — proves an upstream open obligation (typically a Physlib informal_lemma or sorry-tagged statement).
• bridge — proves an equivalence between two formulations so theorems on one side can be reused on the other.
• formalization — first mechanization of a previously known statement. The statement isn't new; the kernel-checked artifact is.
• original — a result whose statement isn't previously in the literature. Held to a strict bar and audited externally before any promotion; most of what a formalization project produces is formalization, not original, and the ledger says so.
• refutation — disproof of a published claim by counterexample.

The running log is in docs/CONTRIBUTIONS.md. For what's next to attack, see docs/OPEN-FRONTIERS.md — open physics problems ranked by our tractability.

A few places to start reading:

• Noether's theorem in general form — noether_general in ApplePie/Action.lean: conservation from any smooth one-parameter symmetry, via genuine Fréchet-derivative variational calculus (the load-bearing step is a Schwarz second-derivative commutation).
• A published physics error caught by theorem proving — the 2HDM vacuum-stability conditions of Maniatis et al. 2006 are refuted by counterexample (via Tooby-Smith / Physlib); see docs/contributions/refutations.md.
• Variational field theory that closes — Klein-Gordon extremality ↔ field equation (ApplePie/FieldTheory/Basic.lean) and sourced Maxwell from gauge-side variation (ApplePie/QED/MaxwellSourced.lean).
• Pre-registered decision rules — one generic, kernel-checked three-branch threshold framework (ApplePie/Epistemology/DecisionRule.lean) instantiated for more than twenty forthcoming measurements, so "what data would refute this hypothesis" is fixed before the data exists.

Layout

Path	What's there
ApplePie/Epistemology/	The discipline layer: Status, Claim, Source, Finding
ApplePie/Adapters/Physlib.lean	The single trust boundary with Physlib
ApplePie/Action.lean	Lagrangians, Noether, conserved currents
ApplePie/Relativity/	SR and the Lorentz-group bridge
ApplePie/StandardModel/Higgs/	SM Higgs stability, 2HDM case study
ApplePie/Cosmology/FLRW.lean	Hubble and deceleration identities
ApplePie/Speculative/	E8, M-theory, asymptotic safety, LQG, causal sets, emergent gravity
docs/ROADMAP.md	Stage-by-stage plan
docs/OPEN-FRONTIERS.md	Open physics problems ranked by our tractability
docs/CONTRIBUTIONS.md	What ApplePie has added upstream
CLAUDE.md	Full architectural and discipline notes

Contributing

If you prove something new, attach a Claim (with proof). If it advances upstream state, also file a Finding and add a line to docs/CONTRIBUTIONS.md. Before pushing:

lake build
bash scripts/audit.sh

Both must be clean.

Citing

If ApplePie helps your work, please cite it. The canonical metadata lives in CITATION.cff — GitHub renders a "Cite this repository" button when this file is present, and reference managers (Zotero, Zenodo, etc.) consume it automatically.

License

Apache 2.0 — same as Lean, mathlib, and Physlib. Patent grant included. Citation in academic work is requested via CITATION.cff, not enforced by the license; no standard OSS license does that.