The funnel
The funnel is a set of written instructions that AI follows to turn a proof Lean has accepted into shorter and shorter versions for different readers. For one Erdős problem that is 152 pages, then 26, then 16, then a half-hour video.
Limits: Lean checks the proof. An expert still has to judge whether each paper and video says the same maths.
Lean is a program that checks mathematical proofs.
