A collection of formal and computational mathematics research, experiments, and verified implementations using Lean 4, Mathlib, computer algebra systems, and related scientific-computing tools.
Each project in this repository formalizes a mathematical result — a theorem, identity, or exact computation — and includes:
- a written account of the mathematics and the proof strategy,
- the Lean source (or equivalent formal artifact) that establishes the result,
- and, where applicable, an independent verification procedure that checks the result mechanically rather than by inspection.
This repository is intended as an ongoing record of formalization work and computational mathematics experiments, and will grow over time as new projects are added.
Released under the Apache License 2.0 (see LICENSE). Third-party dependencies (Lean, Mathlib, and others) retain their own licenses.