litexlang/golitex

何を解決するか

Litexは、自然な数学的記述と形式的検証のギャップを埋めます。従来の証明支援ツールは、数学者が実際に問題を解く方法とは大きく異なる、複雑な型システムの調整や証明スクリプトの学習を要求することが多いです。Litexは、ユーザーが数学的事実を自然で読みやすい順序で記述できる一方で、機械がルーチンな局所的正当化と検証を処理します。

動作方法

Litexは集合論に基づく、事実中心の言語です。数学的対象、定義、および事実の検証済みコンテキストを維持することで動作します。

• 事実マッチング: システムは等価置換、定義、および量化された規則を通じてルーチンな正当化を再構成します。
• 証明プロセス: 複雑なステップに対して、ユーザーは witness（存在命題用）、obtain（既存の証拠を使用）、by contra（矛盾用）、by induc（帰納法用）などのコマンドを使って証明経路を明示的に定義できます。
• 検証: 受け入れられたすべての記述は、なぜ受け入れられたか（たとえば特定の定義や算術規則）と、将来のステップで利用可能な内容を示す証拠を提供します。
• Lean統合: Litexは中間表現（IR）にコンパイルでき、そのIRはLeanコンパイラによって受け入れられ、LeanおよびMathlibのコンテナ上に意味的なラッパーを生成します。

対象ユーザー

• 数学者および学生: 伝統的な形式言語の急な学習曲線なしに、なじみのある記法で検証可能な数学を書きたい人。
• AI研究者: 機械検証可能な局所フィードバックと明示的な仮定を必要とするAI修復ループを開発する開発者。
• 教育者: 現在のコンテキストで特定の事実が正当化されているかどうかを即座にフィードバックできる、認識しやすい数学を提供したい教師。

特徴

• 読みやすい構文: LaTeXスタイルの記法と集合論を使用し、コードを通常の数学的記述に近づけています。
• 事実中心: 証明の置換メカニズムを手動でエンコードするのではなく、数学的結論を述べることに焦点を当てています。
• 検査可能な検証: 詳細診断（-detailモード）を提供し、概念や定理の関係を可視化する関係グラフを生成できます。
• Leanコンパイル経路: 高レベルなLitex開発をLean形式言語に翻訳する道を提供しています。