Moissanite Science
Crystal optics for moissanite and diamond. Total internal reflection, dispersion curves, and 8 novel cut geometries — each with a full physics derivation. 65 theorems · 14 files · fire ↔ brilliance r = −0.973.
Light enters the stone. Mathematics decides where it goes.
969 declarations in Lean 4. Brilliance, fire, structural color, fluorescence, scintillation, and hardness — six axes of beauty, each with a machine-checked proof. For Jill Campbell.
477
theorems
400
definitions
0
sorry
38
files
Opal — Where Chaos Becomes Color
Structural color from Bragg diffraction. Silica nanospheres self-assemble into photonic crystals. The math of play-of-color — Bragg · photonic crystal · close-packed spheres.
The Perfect Stone
The optimal gemstone from first principles. Six beauty axes on a Pareto frontier. NV-center fluorescence. CVD diamond by design. 6 axes · NSGA-II optimizer · 39× vectorized.
Two Books at the Bookstore
We read two popular science books — one on quantum physics, one on machine learning — and checked their mathematics in Lean 4. The receipts are on the page. 969 theorems · 4 sorry (open problems) · 6 seconds to compile.
Explore the verified collection
Each page is a scrollytelling walk through the physics, with every claim anchored to a Lean 4 theorem at a specific file:line in the public repository.