证明一些不等式

hbghlyj

2000 AMC 12 Problem 11
两个非零实数 $a$ 和 $b,$ 满足 $ab = a - b$. 求 $\frac {a}{b} + \frac {b}{a} - ab$.
解: $\frac {a}{b} + \frac {b}{a} - ab = \frac{a^2 + b^2}{ab} - (a - b) = \frac{a^2 + b^2}{a-b} - \frac{(a-b)^2}{(a-b)} = \frac{2ab}{a-b} = \frac{2(a-b)}{a-b} =2$.

在 MiniF2F 中用不同语言的证明形式化。
opendatalab
MiniF2F是奥林匹克级数学问题形式化陈述的数据集，旨在为神经定理证明提供统一的跨系统基准。miniF2F基准目前针对Metamath，Lean和Isabelle，由来自AIME，AMC和国际数学奥林匹克 (IMO) 的488个问题陈述以及高中和本科数学课程的材料组成。

Metamath	${ amc12-2000-p11.0 $e |- ( ph -> A e. RR ) $. amc12-2000-p11.1 $e |- ( ph -> B e. RR ) $. amc12-2000-p11.2 $e |- ( ph -> A =/= 0 ) $. amc12-2000-p11.3 $e |- ( ph -> B =/= 0 ) $. amc12-2000-p11.4 $e |- ( ph -> ( A x. B ) = ( A - B ) ) $. amc12-2000-p11 $p |- ( ph -> ( ( ( A / B ) + ( B / A ) ) - ( A x. B ) ) = 2 ) $= ( cdiv co caddc cmul cmin c2 cexp eqcomd ... $. $} 复制代码
Lean	theorem amc12 2000 p11 (a b : R) (h0 : a ≠ 0 ∧ b ≠ 0) (h1 : a * b = a - b) : a / b + b / a - a * b = 2 := begin field simp [h0.1, h0.2], simp only [h1, mul comm, mul sub], ring, end 复制代码
Isabelle	theorem amc12 2000 p11: fixes a b::real assumes "a \<noteq> 0" "b \<noteq> 0" and "a * b = a - b" shows "a / b + b / a - a * b = 2" using assms by (smt (verit, ccfv threshold) diff divide distrib div self divide divide times eq eq divide imp nonzero mult div cancel left) end 复制代码

hbghlyj

The two IMO-adapted problems
Problem 1: Suppose $a, b, c$ are the sides of a triangle. Prove that $a^2(b + c − a) + b^2(c + a − b) + c^2(a + b − c) ≤ 3abc$.
Problem 2: For $a, b, c$ reals, prove that $(a^2 + ab + b^2)(b^2 + bc + c^2)(c^2 + ca + a^2) ≥ (ab+bc+ ca)^3$.
这些问题的两种解决方案都应用“nlinarith”于正确的参数，这是 mathlib 的一种策略，通过向求解器的上下文添加更多假设来解决非线性算术问题。
mathlib doc
Formalising Mathematics 2022
在博文中说Problem 1的证明来自 Schur 不等式，它给出

1. nlinarith [sq_nonneg (b - a), sq_nonneg (c - b), sq_nonneg (c - a)]

复制代码

Problem 2通过多次应用 Cauchy-Schwarz 解决，然后使用它“发明”的一些不等式，并以上面相同的 nlinarith 表达式结束。

1. theorem imo_longlist_1990_p77
2.   (a b c : ℝ) :
3.   (a * b + b * c + c * a)^3 ≤
4.     (a^2 + a * b + b^2) * (b^2 + b * c + c^2) *
5.     (c^2 + c * a + a^2) :=
6. begin
7.   -- The three initial steps use Cauchy–Schwarz to prove
8.   -- `(a * b + b * c) ^ 2 ≤ (a ^ 2 + b ^ 2) * (b ^ 2 + c ^ 2)`
9.   -- which is required for the final call to `nlinarith`.
10.   let u : euclidean_space ℝ (fin 2) := ![a, b],
11.   let v : euclidean_space ℝ (fin 2) := ![b, c],
12.   have h₀ := real_inner_mul_inner_self_le u v,
13.   simp [u, v, fin.sum_univ_succ,
14.         ←pow_two, ←pow_two, le_of_lt, mul_assoc] at h₀,
15.   -- The model introduces another required cut (i.e. invent
16.   -- the term `0 ≤ (c + a) * (c + a)` and proves it).
17.   have h₃ : 0 ≤ (c + a) * (c + a),
18.   { nlinarith, },
19.   have h₄ := sq_nonneg (a * b + b * c + c * a),
20.   simp [sq, h₀, h₃, mul_add, add_mul] at h₄ ⊢,
21.   nlinarith [sq_nonneg (b - a),
22.              sq_nonneg (c - b),
23.              sq_nonneg (a - c)]
24. end

复制代码

IMO Grand Challenge：让AI在IMO比赛中赢得金牌。

---

AI math theorem proving
thepaper/redian news：近日，Meta AI 构建了一个神经定理证明器 HyperTree Proof Search（HTPS），已经解决了 10 场国际数学奥林匹克竞赛 (IMO) 中的问题，比以往任何系统都更多。此外，该 AI 模型的性能比数学基准 miniF2F 上的 SOTA 方法高出 20%，比 Metamath 基准上的 SOTA 方法高出 10%。
在一定意义上，定理证明要比构建 AI 来玩国际象棋等棋盘游戏更具挑战性。当研究者试图证明一个定理时，可能移动的动作空间不仅很大而且有可能是无限的。相比较而言，在国际象棋或围棋中，这些游戏的一系列走法会被预测出来，即使算法没有给出最好的走法也影响不大。而在定理证明中，当算法走入死胡同就没办法解决了，性能再好的求解器也只是白费力气。
我们用一个例子来说明 HTPS 的优势：假设 a 和 b 都是质因子为 7 的自然数，并且 7 也是 a + b 的质因子，如果假设 7^7 可以整除(a + b)^7 - a^7 - b^7，那么请证明 a + b 至少是 19。

假如让人类来证明的话，他们大概率会用到二项式。而 HTPS 使用 Contraposition 方法，大大简化了方程，然后再检查多种不同的情况。

1. contrapose h₄,
2. simp only [nat.dvd_iff_mod_eq_zero, nat.add_zero] at *,
3. norm_num [nat.mod_eq_of_lt, mul_comm, nat.add_mod] at h₄,

复制代码

如下图为本文模型发现的证明示例，即在 miniF2F 中另一个 IMO 问题的证明：

为了使用计算机编写正式的数学证明过程，数学家最常用的方法是交互式定理证明器（ITP）。下图 1 是交互式定理证明器 Lean 中的一个证明示例：

相应的证明树如下：

给定一个要自动证明的主要目标 g，证明搜索与学习模型和定理证明环境交互以找到 g 的证明超树。证明搜索从 g 开始逐渐扩展出一个超图。当存在从根到叶子均为空集的超树时，即为证明完成。

以下图 5 证明过程为例，假设策略模型 P_θ 和批评模型 c_θ，以目标为条件，策略模型允许对策略进行抽样，而批评模型估计为该目标找到证明的能力，整个 HTPS 的证明搜索算法以这两个模型为指导。此外，与 MCTS 类似，HTPS 存储访问计数 N(g, t)（在节点 g 处选择策略 t 的次数）和每个策略 t 针对目标 g 的总动作（action）值 W(g, t)。这些统计数据将用于选择阶段。

HTPS 算法迭代地重复图 5 描述的选择、扩展、反向传播三个步骤来增长超图，直到找到证明或者超出扩展预算。

Meta 在三个定理证明环境中开发和测试 HTPS：a）Metamath，b）Lean 和 c）Metamath。Metamath 附带一个名为 set.mm 的数据库，其中包含 30k 个人类编写的定理。Lean 附带一个由人类编写的 27k 定理库，称为 Mathlib。最后，由于 Metamath 证明非常难以理解，因而 Meta 开发了自己的环境，称为 Equations，仅限于数学恒等式的证明。

为了模仿人类思维，神经定理证明器需要将特定状态和当前状态（对问题的理解）联系起来。Meta 首先从强化学习开始，该方法与现有的证明助手（proving assistants，例如 Lean）紧密结合。

Meta 将证明的当前状态解释为图中的一个节点，并将每一个新步骤解释为一条边。此外，研究者意识到还需要一种方法来评估证明状态的质量——类似于在棋盘游戏中 AI 需要评估游戏中的特定位置。

受蒙特卡洛树搜索 (MCTS) 启发，Meta 采用在两个任务之间进行循环：在给定证明状态下使用的合理参数的先验估计；给定一定数量的参数后的证明结果。

HTPS 是标准 MCTS 方法的变体，在该方法中，为了探索图，Meta 利用关于图的先验知识来选择一组叶进行展开，然后通过备份修正来改进初始知识。图是逐步探索的，关于图结构的知识随着迭代得到细化。

---

OpenAI Blog
jandan.net 微软资助的OpenAI同天发布了能够证明数学竞赛题的神经网络

OpenAI实际上是独立的工作室，但微软领投了10亿美元。而且，这次发布的神经网络基于微软研究中心开发的程序证明校验语言Lean。

我们为Lean构建了一个神经定理证明器，它学会了解决各种具有挑战性的高中奥林匹克问题，包括 AMC12 和 AIME (美国中学生数学联赛)的问题，以及改编自IMO(国际中学生数学奥林匹克竞赛)的2个问题。

证明器使用语言模型来寻找形式陈述的证明。每次我们找到一个新的证明时，我们都会将其用作新的训练数据，这会改进神经网络并使其能够迭代地找到更难问题的证明方案。

我们在 miniF2F 基准测试中取得了新的最先进水平(41.2% vs 29.3%)，这是一个具有挑战性的高中奥林匹克问题集。我们的方法，我们称之为 陈述课程学习，包括手动收集一组不同难度级别的命题(没有证明)，其中最难的命题与我们的目标基准相似。

最初，我们的神经网络证明器很弱，只能证明其中的几个。我们反复搜索新的证明，并在新发现的证明上重新训练我们的神经网络，经过8次迭代，我们的证明者最终在 miniF2F 上测试时拿到了不错的成绩。

会用柯西不等式的AI
微软资助的OpenAI同天发布了能够证明数学竞赛题的神经网络

形式数学是一个令人兴奋的研究领域，因为

(i) 它的丰富性，让您可以证明需要推理、创造力和洞察力的任意定理，以及

(ii) 它与游戏的相似性——人工智能在游戏领域取得了惊人的成功——因为它具有自动化确定证明是否成功的方法(即，由正式系统验证)。如下面的简单示例所示，正式陈述需要生成一系列证明步骤，每个证明步骤都包含对策略的调用。

正式系统接受的工件语句是底层的(如汇编代码)，人类难以生成。策略是从更高级别的指令生成此类工件以帮助形式化的搜索过程。

我们观察到，在我们的训练过程中出现了生成作为战术参数所需的原始数学术语的能力，如果没有神经语言模型，这是无法完成的。在一个证明里，证明器基本掌握了数学归纳法的表述。

我们还观察到，我们的模型和搜索程序能够生成链接多个非平凡推理步骤的证明。在证明中，模型首先使用导致存在性陈述 (∃ (x : ℝ), f x ≠ a * x + b) 的对立。然后它使用 (0 : ℝ) 为它生成一个特例，并通过利用norm_num策略完成证明。

我们的模型经过陈述课程学习训练，能够解决培训教科书以及 AMC12 和 AIME 比赛中的各种问题，以及改编自 IMO 的 2 个问题。

但形式数学涉及两个主要挑战，使得强化学习的简单应用不太可能成功。

(i) 无限的动作空间：形式数学不仅有一个非常大的搜索空间(比如围棋)，它也有一个无限的动作空间。在证明搜索的每一步，模型必须不是从行为良好的有限动作集中进行选择，而是从一组复杂且无限的策略中进行选择，其中涉及必须生成的外生数学术语(自己定义符号，用作诸如“存在一个 xx st ...”之类的步骤中使用的对象，或在证明中间引入和链接引理)。

(ii) 缺乏自我博弈：与 2 人游戏相反，证明者不是与对手对抗，而是与一组要证明的陈述对抗。当面对一个太难的陈述时，没有明显的重构可以让证明器生成中间更容易解决的引理。这种不对称性阻止了在 2 人游戏中成功的自我游戏算法的幼稚应用。

在我们的工作中，我们通过在搜索证明时从语言模型中采样动作来解决无限动作空间问题。语言模型能够生成策略调用以及通常需要作为参数的原始数学术语。我们解决缺乏自我游戏的基础是观察到自我游戏在 2 人游戏中的关键作用是提供无监督的课程。我们建议用一组不同难度的辅助问题陈述(不需要证明)来代替这种无监督的课程。我们的经验表明，当辅助问题的难度足够时，我们的训练程序能够解决越来越难的问题，最终推广到我们关心的问题集。

虽然这些结果非常令人兴奋，因为它们证明了深度学习模型在与正式系统交互时能够进行非平凡的数学推理，但AI距离最出色的人类中学生还差得远，只是偶尔能，而非始终如一地解决具有挑战性的奥林匹克问题。尽管如此，我们希望我们的工作能够激发该领域的研究，特别是针对 IMO 大挑战，并且我们提出的陈述式课程学习方法将有助于加速自动化推理的总体进展。
论文

---

arxiv.org/pdf/2210.12283.pdf
机器之心 / 51cto DSP新方法将机器证明成功率提高一倍在最近的一项工作中，谷歌的吴宇怀 (Yuhuai Tony Wu)等研究者设计了一种叫做 DSP（Draft, Sketch, and Prove ）的新方法，将非形式化的数学证明转化为形式化的证明，从而同时具备形式化系统提供的逻辑严谨性和大量的非形式化数据。
今年早些时候，吴宇怀与几位合作者使用了 OpenAI Codex 的神经网络进行自动形式化工作，证明了用大型语言模型将非形式化语句自动翻译成形式化语句的可行性。DSP 则更进一步，利用大型语言模型从非形式化证明中生成形式化证明草图。证明草图由高层次的推理步骤组成，可以由交互式定理证明器这样的形式化系统来解释。它们与完整的形式化证明不同，因为它们包含无理由的中间猜想的序列。在 DSP 的最后一步，形式化证明草图被阐述为一个完整的形式化证明，使用一个自动验证器来证明所有中间猜想。

吴宇怀表示：现在，我们展示了 LLM 可以将其生成的非形式化证明转化为经过验证的形式化证明

方法
方法部分描述了用于形式化证明自动化的 DSP方法，该方法利用非形式化证明来指导自动形式化定理证明器的证明草图。这里假设每个问题都有一个非形式化命题和一个描述该问题的形式化命题。整体 pipeline 包括三个阶段（如图 1 所示）。

非形式化证明的起草

DSP 方法的初始阶段，包括根据问题的自然数学语言描述（可能用 LATEX）为其寻找非形式化证明。由此产生的非形式化证明被看作是后续阶段的草稿。在数学教科书中，一般都会提供定理的证明，但有时会缺失或不完整。因此，研究者考虑了与非形式化证明的存在或不存在相对应的两种情况。

在第一种情况下，研究者假设有一个「真实的」非形式化证明（即由人写的证明），这是现有数学理论形式化实践中的典型情况。在第二种情况下，研究者做了一个更普遍的假设，即没有给出真实的非形式化证明，并且用一个经过非形式化数学数据训练的大型语言模型来起草证明候选。该语言模型消除了对人类证明的依赖，并能为每个问题产生多种备选解决方案。虽然没有简单的方法来自动验证这些证明的正确性，但非形式化证明只需要在下一阶段对生成一个好的形式化证明草图有用。

将非形式化证明映射为形式化草图

形式化证明草图对解决方案的结构进行编码，并撇开低层次的细节。直观地说，它是一个部分证明，概述了高层次的猜想命题。图 2 是一个证明草图的具体例子。尽管非形式化证明经常撇开低层次的细节，这些细节不能在形式化证明中排出，这使得非形式化证明到形式化证明的直接转换变得困难。相反，本文建议将非形式化证明映射到共享相同高层结构的形式化证明草图上。证明草图中缺少的低层次细节可以由自动证明器来填补。由于大型非形式化 - 形式化平行语料库不存在，标准的机器翻译方法不适合这项任务。相反，这里使用一个大型语言模型的小样本学习能力。具体来说，用了一些包含非形式化证明及其相应的形式化草图的例子对来 prompt 该模型，然后是一个有待转换的非形式化证明，然后让模型生成后续的 token，以获得所需的形式化草图。这个模型称为「自动形式化器」。

证明草图中的公开猜想

作为这个过程的最后一部分，研究者执行现成的自动证明器来填补证明草图中缺失的细节，这里的「自动证明器」是指能够产生形式上可验证的证明的系统。该框架对自动证明器的具体选择是不可知的：它可以是符号证明器（如启发式证明自动化工具）、基于神经网络的证明器或者混合方法。如果自动证明器成功地填补了证明草图中的所有空白，它就会返回最终的形式化证明，可以对照问题的规格进行检查。如果自动证明器失败（例如，它超过了分配的时间限制），则认为评估是不成功的。