A followup to my previous video, in which I now see how #Claude and #o4mini do at formalizing a slightly different proof of the same algebraic implication, after being given the initial informal and formal proofs as reference. www.youtube.com/watch?v=zZr5...

A video on an actual formalization task from my Polynomial Freiman Ruzsa (PFR) project, which is sufficiently tricky (and sufficiently far from existing training data of current models) that one still has to largely formalize these proofs by "hand": www.youtube.com/watch?v=6uLX...