What if a translation could be checked the way software is checked? One verse of Sanskrit can be translated three grammatical ways that disagree about the nature of reality, and for fifteen centuries the commentary has been the only referee. This book brings objective verification into that most subjective of arts.

It tells the story of the complete first book of Bhartrhari's Vakyapadiyam, the Brahmakanda, whose every verse now carries a reading proved adequate against its commentary in the Lean theorem prover, with 361 plausible mistranslations refuted by compiled theorems. Nothing rests on the author's authority: every verdict rebuilds from public source in seconds.

The same method Google DeepMind's AlphaProof used to reach the Mathematical Olympiad, pointed at the oldest questions about words. Written for five kinds of reader at once, from AI engineers wrestling with hallucination to lovers of Sanskrit, it assumes no prior knowledge of either. It teaches from first principles the two traditions it joins: Panini's grammar and the dependent type theory that powers modern proof assistants, meeting in Navya-Nyaya, the formal logic India built centuries before formal logic had that name.