Post by @jdw@mathstodon.xyz

2026-08-10 10:14 UTC

@atif@mathstodon.xyz @maxpool@mathstodon.xyz @tao@mathstodon.xyz As many of my friends can confirm, I was predicting that AI would outperform humans in mathematics already ~10 years ago (and I had a number of heated debates about this back then). This was roughly the time when I learned about proof assistants and when programs like AlphaZero and AlphaGo achieved new peek performances in games like chess and Go. I must admit though that I expected the method for solving math would be old fashioned reinforcement learning, the game state being a Lean context window, allowed moves being applicable Lean tactics and a winning move being a completed proof. The analogy between making progress on a math problem by stating and proving a helpful intermediate result and improving the own position in chess or Go seemed very obvious to me. I just couldn't answer the question who would pay for the development of such a system. I did not predict that natural language processing would be solved first and that the math AI would be the same program that would spam social media networks with political propaganda and render graphics designers, copywriters, composers and software developers jobless together with mathematicians.

Replies (2)

@jdw@mathstodon.xyz 2026-08-10 10:28

@atif@mathstodon.xyz @maxpool@mathstodon.xyz @tao@mathstodon.xyz (I also did not predict that the then-liberal class of US tech oligarchs would turn to right wing authoritarianism under a new fascist regime in the US and would spend all of their billions and more to create this theorem-proving machine.)

Open ##5161031
@atif@mathstodon.xyz 2026-08-10 18:05

@jdw@mathstodon.xyz thanks for the comment! i thought the RL+Lean approach isn’t completely dead? it may seem unnecessary today, but as many have observed, who knows how ai for mathematics will look like after the labs squeeze the last bit of marketing points out of mathematics. however, my point was somewhat different, and perhaps it came across, but im happy to say more anyway: my question was a response to the argument that we are close to the point where human input won’t be needed at all (the meme was used in this sense when i saw it), which is different from the question whether humans are being outperformed. the machines wield the existing mathematics very well, but they are yet to come up with new mathematics to help them solve a problem. this is the “bad at theory building” argument. if we are to believe that soon no human input will be needed, that means(?) data is rich enough with good ideas, that empower ai to come up (reasonably fast) with new radical ideas. it’s not obvious to me that there’s enough good ideas in the data! it’s not obvious to me that a machine trained on the current mathematical corpus can render us jobless. it’s not obvious to me that we are not lacking a couple more revolutions and breakthroughs. so i wondered, did anyone share this sentiment pre 2022: “there’s no big ideas left to discover in mathematics”? even if tomorrow we see theory building, there’s another level: rebuilding. i think there’s lots of technical debt in theories and we roll with it, but im convinced that the theories will go through iterations of rebuilding (as they do). i think it takes another big non-obvious leap if we are to project a future in which the machines can do that as well @maxpool@mathstodon.xyz @tao@mathstodon.xyz

Open ##5161032