Case study: proving sqrt(2) irrational with LPTP and an LLM
用LLM辅助逻辑编程定理证明器,给出根号2无理性的形式化证明,AI与数学推理的跨界案例。
arXiv:2607.21187v1 Announce Type: cross Abstract: We present the interactions with an LLM (Large Language Model) aiming at proving that the square roo…