[Invited Talk]: I will describe my experiences with “vibe formalizing”: having Claude Code autoformalize mathematics, both with a scan of a textbook as its source and just from its own understanding of the mathematics, and both fully automatically and with me watching and giving it a push now and then.

The results are impressive, but Claude seems to lack a feeling for the bigger picture, and for that reason the formalizations that get produced are often less than elegant, to say the least.

This raises the central question of this talk: even when the proof assistant accepts every proof, how can one assess whether the “AI slop” that gets produced faithfully captures the intended mathematics? In this sense a formally verified formalization can still be “unsound”.

I will argue that the key to making vibe formalizing more trustworthy is to cleanly separate the definitions and statements from the proof details so they can be easily reviewed, and to tightly integrate the formalization with the source text, to constrain the AI from drifting or complicating things.