Proofs of physics.
Shown working.
A theorem goes in. A machine-checked proof comes out — with the whole derivation still attached.
Decompose
A TheoryState — postulates, approximation regime, conserved quantities, symmetries — decides where the theorem splits. Not token similarity.
Prove
Each subgoal gets its own loop: search Physlib and Mathlib, write Lean tactics, read the rejection, try again.
Verify
The Lean 4 kernel decides. Nothing is reported as proved that it did not accept, and every rejection is kept verbatim.
Every step, as it happens.
A subgoal stalls, the failure is diagnosed as a missing hypothesis, the blueprint is rewritten around it, and the proof closes — drawn in the chat as it happens. Nothing here is staged: the events, the Lean lines and the timings are lifted from a real run.
- Library lookup
- TheoryState
- Blueprint · 3 subgoals
- s = 100 m
- t = 10 s
- v = 20 m/s
- Revise · +1 subgoal
- a ≠ 0
- v = 20 m/s
- Assembly
theorem car_overtakes_truck (a u : ℝ) (ha : a = 2.0) (hu : u = 10.0) : let s := 2 * u ^ 2 / a let t := 2 * u / a let v := a * t s = 100.0 ∧ t = 10.0 ∧ v = 20.0 := by intro s t v have hs : 2 * u ^ 2 / a = 100.0 := by subst ha; subst hu; norm_num have ht : 2 * u / a = 10.0 := by rw [ha, hu]; norm_num have ha_ne : a ≠ 0 := by rw [ha]; norm_num have hv : a * (2 * u / a) = 20.0 := by rw [ha, hu]; field_simp exact ⟨hs, ht, hv⟩Bring a theorem.
Describe the physics in your own words. The console proposes the Lean 4 statement, runs the pipeline in front of you, and hands back the file the kernel accepted.