One thing he does point out closer to the conclusion is that currently they haven't found LLMs to be particularly useful, and notes also that AlphaProof is currently not quite there yet in writing succinct proofs. Nonetheless, he seems to be optimistic and thinks that these models will improve quickly.

I wanted to use this moment to be simply impressed by how much 'intelligence' we can get out of many people working towards a common goal with the same ideals. The most recent and biggest advances and progress in machine-assisted proofs has been, according to Tao, the improvements in more traditional communication/organisation/automatisation processes. This enabled many humans to put their efforts together and establish the foundations for future mathematics. So incredible.