RosettaMath: Reading, Running and Proving Mathematics from LATEX

Abstract

The translation of theoretical mathematical models into executable code remains a persistentbottleneck in computational science. While LATEX serves as the standard for sharing algebraicequations and algorithms, its representation is fundamentally disconnected from the explicit logicrequired by programming languages like Python. We present RosettaMath, a zero-dependencytranslator that converts a strict subset of LaTeX—specifically mathematical expressions and algo-rithmic pseudocode—directly into functional Python. Notably, RosettaMath is self-hosting; the coretranslation engine is written in the very LATEX subset it processes and bootstraps itself to a fixedpoint without external libraries. Beyond its mechanical translation capabilities, RosettaMath isdesigned as an educational bridge. By semantically mapping dense physics and mathematical con-ventions to explicitly named variables and scientific libraries (such as mapping standard symbols toscipy.constants), the tool demystifies standard notation for software developers while simultaneouslyteaching programmatic logic to mathematicians. RosettaMath offers a novel approach to literateprogramming, ensuring that the equations published in research are the exact algorithms executedin simulation.RosettaMath provides a custom PyQt interface for interactive exploration of equations, and itsown LEAN engine (lean4.py) a Calculus of Constructions kernel with de Bruijn indices, inductivefamilies with generated recursors—equality among them—an untrusted elaborator that infers im-plicit arguments by Miller pattern unification with postponed constraints, and a LATEX statement lan-guage, so that a theorem about a Python function is stated as \forall x \in \text{Nat}, x = x,or proved by induction, and checked by a kernel small enough to read in one sitting.We argue that these three pieces, precisely because they are small, local, open and written inthe language students already learn, form a practical foundation for mathematics and programmingeducation at every level—from a child clicking on a Greek letter to an undergraduate proving sym-metry of equality to a researcher graduating to Lean—and that the same small trusted kernel pointstoward verified systems software when its statement language becomes the contract language.