Synthetic differential geometry treats infinitesimals as actual objects — not limits, not epsilons, but elements of a ring satisfying d squared equals zero. The theory has existed since the 1970s. Formalizing it in Lean 4, a modern proof assistant, should have been a translation exercise.
It wasn't. Most of the proofs are new.
The standard textbook proofs did not survive the translation into constructive type theory. The gaps were not errors — the original arguments relied on informal reasoning steps that are valid in classical mathematics but unavailable in a constructive setting. Each gap required a genuinely novel proof strategy, not a patch.
The central result is a formalized multivariable Taylor theorem with expansions around infinitesimal neighborhoods. Getting there required building the theory from scratch within mathlib, Lean's mathematical library. Mathlib was designed primarily for classical mathematics, and the authors discovered it could support constructive reasoning — a capability that was not an intended design goal but emerged from the library's generality.
This illustrates something about the relationship between formalization and knowledge. The common view is that proof assistants verify — you feed them a known theorem and they check it. But verification under stricter rules can force discovery. When the destination is fixed (Taylor's theorem) but the path constraints are tighter (constructive logic), the system demands new routes that human mathematicians had never needed to find.
The implication extends beyond this specific formalization. Any time you translate knowledge into a system with different rules — a different logic, a different programming language, a different organizational framework — the translation failures are not bugs. They are sites where the original knowledge was incomplete in ways invisible under the original rules. The tool reshapes what it was meant to merely record.