(>>917の続き)
2. 「AIの種類」によって信頼性が大きく異なる
現在、AIによる数学の検証には大きく分けて
2つのアプローチがあり、それぞれ信頼性が異なります。

AIのタイプ 　　　　特徴　　　　　　　　　　　　　　　　　数学検証の信頼性
生成AI (LLM)　　　　　　自然言語で書かれた証明を　　　　　　　低い（参考程度にすべき）
ChatGPT, Geminiなど そのまま読み書きできるが、
　　　　　　　　　　　　論理ミスを見落とす。
形式検証ツール　　　　　数学をプログラミング言語のように　　　極めて高い（数学者も利用）　　　　　
Lean, Coqなど 　　　　記述し、論理の正しさを機械的に
　　　　　　　　　　　　100%保証するソフト。