MathCode terminal agent automates Lean 4 theorem formalization and proving

MathCode converts natural language math problems into Lean 4 theorems using a persistent REPL that reduces compile check latency from 30s to 0.4s. The agent maintains reusable theorem and axiom libraries while integrating with an Obsidian knowledge graph for formal proof management.