This is indeed an excellent talk, and I think contains the seeds of a path forward through the AI thicket. When tested against only "vibes," AI can generate reams of slop. But when tested against hard ground truth, in this case rigorous mathematical formalism, possibilities abound.
Raph Levien
#Math Professor Emily Riehl shows in her speciality that "vibe proving" with LLMs is consistently &insidiously wrong, and threatens to swamp a struggling peer review system:
youtu.be/fzxW2XJS6SE
But! "computer aided formalisation" building on GOFAI symbolic methods may revolutionise complex proofs
