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…