AIs rushing to the proofs
A “Feature” article in Nature (21 May 2026) and a long article in the New York Time (June 8, 2026) are both covering the sudden intrusion of AIs in proving or disproving mathematical conjectures… Genuine, hard, conjectures likes Erdös problems. Specialised AIs like Alethia, Math Inc., AlphaProof are hacking at existing open problems and a benchmark collection of problems whose solutions are not available (yet) called First Proof has been recently gathered, solved by OpenAI, and is soon to be extended. In an earlier interview with Nature (27 April 2026), Terry Tao acknowledges the tectonic shift represented by this intrusion and how a mathematician’s skill need evolve. (This is also the starting point of the NYT story. ) A side issue of this is that reviewing the proofs thus produced by an AI may prove inhumane if it reaches hundreds of pages, which also relates to the un-academic (?) tendency of AIs companies to over-blow the results produced by their machines. For the times they are a-Changin…
June 23, 2026 at 1:10 pm
Having been inspired by examples shown by (e.g.) Thomas Bloom at an AcadMathSci meeting of the progress AI is making on the Erdos problems (his website has somehow become a magnet for AI proof merchants), I have been testing the capabilities of Claude and ChatGPT to deliver statistics-relevant proofs. Coincidentally they claim today to have achieved an extension of your proof of nested sampling CLT under ‘realistic’ conditions of MCMC live point refreshment and tail evidence summary/stopping. Might still be a load of rubbish though, I’m yet to satisfy myself that it’s correct. I was drawn back into nested sampling because Johannes Buchner shared with me a human made proof of nested sampling convergence for the RadFriends algorithm.
https://diatribo.netlify.app/posts/2026-06-23/
June 23, 2026 at 4:27 pm
Very interesting news!!! I am also re-working on nested sampling following a summer project and looking at ways of assessing the variability of the thing, less asymptotically than the CLT.