Numina Fuse: Interactive Autoformalization in Lean 4.

arXiv:2610.33860v1 Announce Type: new Abstract: Numina Fuse is an agent-native application for formalizing mathematics in Lean 4. Since Lean can compile while not representing its intended informal meaning, and agents now write Lean faster than people can read