Formally Verified AI: What Machine-Checked Proofs Reveal About LLM Compression

​Speaker 

​Sean Simms 

​Founder & CEO, Manazo Labs (HarmonicQ Inc.) — Halifax, Nova Scotia 

​Most AI research is tested by running experiments and comparing results on standard tests. But what happens if you check a published AI method using strict, formal math instead of just experiments? This talk walks through a real example: we used the Lean 4 proof system to mathematically verify Google Research’s TurboQuant method. The full proof includes 8 files and 58 machine‑checked results, with no gaps or assumptions. While doing this, we also fixed three issues in the original paper: we improved one of the constants by 43%, we put a clear limit on an assumption that was previously left open‑ended, and we proved that one of the design choices in the method is actually the best possible. The talk ends with a live demo showing how these verified results can be used in real AI systems.