Try to Prove Math with Computers (chillphysicsenjoyer.substack.com)

A developer working on PhysLEAN (formalising physics in the LEAN theorem prover) walked readers through a toy example to demonstrate how mathematicians “prove” statements with computers. Using LEAN’s lemma syntax, they encoded the claim 0 ≤ 2 and solved it interactively by applying previously proved theorems: zero_leq_n (which asserts 0 ≤ a given 1 ≤ a for natural a) and one_leq_two. The key steps show how the apply tactic performs pattern matching (instantiating a = 2), spawns subgoals (here 1 ≤ 2), and is resolved by another lemma. The post also highlights practical tooling—VS Code integration, Loogle for searching Mathlib’s large theorem base—and notes that many such numeric facts are now handled by Mathlib automation (e.g., norm_num) in one line. For the AI/ML community this is a compact illustration of formal methods meeting automation: theorem provers structure proofs as goal-oriented search problems, with tactics and libraries enabling huge reuse and mechanised rigor. That structure makes these systems attractive testbeds for ML-driven automation (auto-tactic synthesis, neural theorem provers, search-guided proof agents) and for building verified scientific software (e.g., formally checked physics). The example captures the essentials: declarative lemmas, hypothesis management, pattern-driven instantiation, and a gradient from manual tactic play to fully automated library tactics—useful context for anyone exploring ML-assisted formal verification.