LeanTeX
Core idea
LeanTeX analyzes proof structure and translates it into an intermediate representation resembling tactic mode, making it easier to produce structured mathematical explanations. It is a tool that converts Lean 4 programs into LaTeX documents.
Current scope
The current methodology starts with propositional logic and is designed to extend to richer proof systems. A team effort alongside my brother Logan.