fun Chess Monte Carlo Simulation Tracking the 2026 Candidates with dynamic player strength, one million simulated tournaments per round. Formalization of Tao's Analysis I in Lean 4 A from-the-axioms-up Lean 4 formalization of Terence Tao's Analysis I, covering both the main text and the exercises with no outside libraries.
