摘要:數(shù)學的人工智能不僅在智力上引人入勝,而且在科學、工程和其他領域對人工智能的發(fā)現(xiàn)也至關重要。在AL4MAST上的大量工作已經(jīng)在NLP中鏡像了技術,特別是在精心編排的數(shù)學數(shù)據(jù)集的文本形式上訓練大型語言模型。形式數(shù)學推理作為一種補充而又不太被探索的途徑,它以證明助理等形式系統(tǒng)為基礎,能夠驗證推理的正確性并提供自動反饋。在這篇立場論文中,我們提倡形式數(shù)學推理,并認為它對于提升到下一個層次是不可或缺的。近年來,我們看到在使用人工智能進行形式推理方面取得了穩(wěn)步的進展,包括定理證明和自形式化等核心任務。以及新興的應用程序,如可驗證的代碼生成和硬件設計.然而,要真正掌握數(shù)學并取得更廣泛的影響,人工智能還需要解決重大挑戰(zhàn)。我們總結現(xiàn)有的進展,討論尚未解決的挑戰(zhàn),并展望衡量未來成功的重要里程碑。在這個正規(guī)數(shù)學推理的轉折點,我們呼吁研究界團結起來,推動這一領域的變革性進展。我們呼吁研究界共同推動這一領域的變革性進展。我們呼吁研究界共同推動這一領域的變革性進展。