用大模型辅助证明√2为无理数，全程可读可验。
Case study: proving sqrt(2) irrational with LPTP and an LLM
- 基于自然演绎的逻辑编程系统，逐步构建证明框架。
- 大模型生成部分证明步骤，经系统严格验证通过。
- 适合对形式化证明与AI协作感兴趣的读者。
我们通过一个大型语言模型（LLM）在逻辑编程（LP）环境中尝试证明√2不是有理数。从几个基本的纯逻辑编程谓词定义出发，利用基于自然演绎的逻辑程序定理证明系统（LPTP）来陈述和验证逻辑程序的性质。在本案例研究中，我们在LPTP中草拟了常规的√2无理性证明过程，随后描述了与大模型的交互细节。最终获得了一个完整的正式证明，其中部分内容由大模型生成，全部由LPTP进行严格验证。
原文摘要 · Abstract (English)
We present the interactions with an LLM (Large Language Model) aiming at proving that the square root of 2 is not a rational number in an LP (Logic Programming) context. We start from a few basic pure logic programming predicate definitions. We rely on the LPTP (Logic Program Theorem Prover) system for stating and proving properties about logic programs. As the proof language of LPTP is based on natural deduction, the proofs are human readable. In our case study, we sketch in LPTP the usual proof showing the irrationality of the square root of 2. Then we describe the interactions we had with the LLM. We end up with a complete formal proof, partially generated by an LLM and fully proof-checked by LPTP.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。