alex 还是差距蛮大的，严格来说ai做出来的是两道代数，一道数论和一道几何。首先来讲，ai做几何已经比较成熟了，alphageometry在此之前就能够解决绝大多数比较容易的几何问题以及一些逻辑链相对比较短（差不多9-10步左右）的问题。然后12两道题目相对于解答较为简练，同时不涉及模糊的操作（比如不等式），所以通过llm和lean交互就能够快速解决，第六题也是一样，不过据说第6题跑了好几天时间。
大概讲一下ai做数学题的基本过程，首先是将一些数学对象转换成lean代码，然后再建立lean的定理库，之后将问题转换成形式化语言，然后判断当前可以当前的条件可以使用怎样的定理或者策略（tactic），然后就用定理库生成一个结论的库，然后查重，删去重复生成的结论，这样就得到了问题通过一步转换可以生成的闭包，然后反复跑，直到做出问题，但这样有一个问题，就是比如说平面几何，需要构造辅助线（也就是说题目中原本的一些条件被删去了），这个时候就需要他自己补全，但是这件事情显然不是跑定理库能解决的问题，所以有人就想到一个办法，用llm生成一些idea，然后加上这些idea的条件再去跑。
但这件事情就更不靠谱了，llm生成思路本来就是一个玄学的事情，平面几何的辅助线从道理上来讲还是有限的那些（指竞赛题），llm跑几遍试错就好了，但是其他的数学问题靠这个东西就不大靠谱了。而且另一个问题就是耗时，步骤增加后，生成的结论和原来的条件共同构成了下一次运行的初始条件，再加上llm要生成idea，所以有的步骤甚至要反复做。第三个问题是，构造性的问题ai目前几乎束手无策，不等式的问题也只能做一些线性的东西。
