savanty investigates whether natural language can reliably interface with mathematical solvers. It implements a pipeline from English problem descriptions to formally provable solutions, studying the gap between human intent and mathematical guarantees that pure LLM output cannot provide.