讨论的核心是一篇文章。文章认为，人工智能，尤其是采用 Lean 语言和形式化证明助手的系统，可能正在改变数学，并迫使数学家直面传统角色的消失。评论者围绕这究竟会给数学界带来一场存在性危机，还是仅仅意味着工具发生改变展开讨论；有人将这种变化与软件工程的发展相比。 许多人认为，人工智能可以加快研究、验证证明，并实现超越人类能力的发现；也有人强调其局限性、不可靠的输出、极其庞大的搜索空间，以及人类洞察力和意义的流失。经济方面的分歧尤其明显：一些人欢迎新工具带来的生产力，另一些人则警告失业、工资受压、财富高度集中，以及传统学术研究经费减少等问题。 不少评论者将数学比作绘画或其他创造性职业，认为即使常规发现被自动化人类的想象力、判断力、原创性和文化参与也可能变得更加重要。更广泛的分歧在于，社会能否通过教育、新制度、更完善的劳动保护和公共投资来适应这一变化，还是 powerful 的公司和资助方会瓜分人工智能带来的几乎全部收益。