@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