A memory-efficient, single-GPU training and inference architecture for formalizing natural language mathematics into Lean 4 statement code using quantized Mixture-of-Experts, persistent Lean REPL compiler feedback, and dual-tier retrieval augmentation.

Can tiny quantum neural networks outperform massive deep learning models? We don’t know (yet), but we collected everything you need to know about the topic, and through a set of experiments we explore the most promising application: PINNs.