Theorem.chat年頃
Theorem.chat は数学的な主張を受け入れ、それを解決しようとします。あなたは主張とそれが満たすべき基準を述べます。AI モデルのパネル - あなたが望むだけ、あなたが望むベンダーから - がそれを攻撃し、さらにモデル審査員が一人追加されます。その論証は Lean 4 で Mathlib に対して形式化され、リーンカーネルはそれが証明されるかどうかを決定します。最後のステップは、生成です。
なぜカーネルを他のモデルではなく
モデルに難しい質問をすると、正しいかどうかの流暢な答えを得ることができます。複数回質問すると、しばしば同意します。これは確証のような感じですが、そうではありません。モデルは訓練データを共有し、盲点を共有します。第 1 回目のモデルをチェックする第 2 回目のモデルは、同じ判断であり、話し合いができるのです。リーンカーネルはできません。公理と Mathlib から命題を導出するか、それともしないか、信頼度は結果に影響しません。
形式的証明を偽造する通常の方法はチェックされ拒否されます。sorryに穴を開けた証明、native_decideに呼びかけてカーネルに信頼の上で計算を行わせた証明、または静かに新しい公理を導入した証明は、成功として計算される代わりに検出され拒否されます。
パネルの実際の機能は
論争は安価な部分です。パネルは文献を使っています。arXiv、OpenAlex、Crossrefなどです。それで、悪い結果を再導出するのではなく、既知の結果を引用します。計算にはSageMathとPARI/GP、SMT解法にはZ3とCVC5、構築したシーケンスを識別するためのOEISのルークアップ、ネットワークアクセスがないサンドボックス型Python環境があります。予想は誰もが証明を試みる前に10,000のケースでテストできます。反例は議論をすぐに終わらせます。
証拠を持って 口説くのは やめて
これは、 論理的に正しい結果を得るために、 論理的に正しい結果を得るため
君がバランスを取った
基準はあなたが選ぶものであり、審査員は文字通りそれを持っています。注意深い専門家が受け入れるものを尋ねると、あなたはそれを得ます。すべての仮定を述べた完全な推論論争を尋ねると、あなたはその代わりにそれに対して判断されます。賞の提出に対して課せられる基準を尋ねると、正直な結果は、通常、パネルがどこで不十分だったかの正確な説明である。それは、あなたがいずれ自分でチェックしなければならない自信ある主張よりも価値がある。
これは、未解決問題を解決するマシンではありません。 解決されていない論理を解決されたと認めることを拒否し、どのステップが失敗したかを正確に伝えるマシンです。
形式化の失敗は有用な出力である
リーンが証明を閉じないときは、残っている正確なゴールを得ることができます。実際には、それはほとんど常に非公式な論争が手を振った場所であり、文字通りの版を読む人は皆、手を振ったと思うでしょう。そのゴールは、攻撃するのに最も適した席に渡され、すでに試みたことと共に、他の何もありません。モデルは、 詰まったときにスラッシュし、全額をかけて自分を再定義します。代わりに、特定の質問を通過すると、通常、トークンの一部でブロックを解除します。
長い仕事は生き残る
これは、パネルが設定したすべてのレムが証明と共有された大帳に入るようにするためで、結果は一度書き込まれ、再導出されることはなく、死角は記録され、誰も戻ってこない。マッチはサーバ側で実行され、予算、プロバイダの停止、タブを閉じたために一時停止され、停止したところで再開されます。
これは何のために？
定理は推論的な言葉です。このサイトは数学、論理学、理論計算機科学、理論物理学、経済学の分野に作られました。これらの分野では、主張は証明によって決定されます。生物学、医学、化学、社会科学の経験的な問題は定理を生み出すのではなく、発見を生み出します。どんな形式化もそれを決定しません。私たちの姉妹サイトreferee.chatは、同じパネルと審査員プロセスを実行します。リーンステップを使わずに、正確にその問題に対して。