这开始发生了。 像Aristotle这样的AI工具，通过@leanprover内置形式验证，将大大降低成为数学家的门槛。 这样一来，我们将看到数学家数量的巨大增加以及生成的数学内容总量的增加。