Belangrijkste concepten
整数の性質に関する様々な定理を自動的に形式化する。
Samenvatting
本論文では、整数の性質に関する定理を自動的に形式化するフレームワーク「GFLean」について説明する。GFLeanは、文法フレームワーク「Grammatical Framework (GF)」を使用して入力を解析し、Lean定理証明システムの入力に変換する。
具体的には以下の手順で動作する。
- 入力の「Simplified ForTheL」文を解析し、抽象構文木(AST)を生成する。
- AST に対して簡単化処理を行う。
- 簡単化されたAST をLean式に変換する。
- Lean式をGFを使ってリニアライズする。
GFLeanは、数学教科書の第3章から62の定理のうち42の定理を自動的に形式化することができる。入力文は、整数の奇偶性、不等式、論理演算などを含む比較的単純な数学的記述である。GFLeanの現在の制限は、複雑な言語構造や動的な語彙の拡張に対応できないことである。今後は、ルールベースの翻訳システムと機械学習翻訳システムを組み合わせることで、より堅牢な自動形式化ツールを構築することを検討している。
Statistieken
x ^ 2 + 1 > 0
((x ^ 2) - (2 * x)) + 2 ≤ 0
((x ^ 2) + 1) / r ≤ 1
((x ^ 3) - (5 * x)) - 1 ≥ 0
((x ^ 2) + (y ^ 2)) + (z ^ 2) < (((x * y) + (x * z)) + (y * z))
1 - (n ^ 2) > 0
((5 * x) - 7) は偶数
((5 * x) - 7) は奇数
((7 * x) + 5) は奇数
15 * n は偶数
((5 * x) - 11) は偶数
((7 * x) + 4) は偶数
((3 * x) + 1) は偶数
((n + 1) ^ 2) - 1 は偶数
(n ^ 2) + (3 * n) + 5 は奇数
a * b は偶数
Citaten
"If x < 0, then x^2 + 1 > 0."
"If 0 < x < 1, then x^2 - 2x + 2 ≠ 0."
"If a, b and c are odd integers such that a + b + c = 0, then abc < 0."
"If n is an odd integer, then 3n + 7 is an even integer."
"If n is an even integer, then -5n - 3 is an odd integer."