撰写 Lean 证明脚本

hbghlyj

欢迎在定理区撰写 Lean 证明脚本：
所有代码块均会被识别为 Lean 代码并高亮显示；
每个代码块右上角都会出现

• “复制代码”按钮
• “在 Lean 在线 Playground 打开”按钮，即可在浏览器中分步检查、运行你的证明！

由计算机检查每一步推理，杜绝人为疏漏。
如何开始？在编辑框输入三个`号，粘贴或编写你的证明脚本；
保存/提交后，点击右上角按钮，即可复制或在线运行。

---

在 Kimina Prover 演示的网页界面中，页面顶部配置了一个用于输入自然语言数学命题的文本框及“Formalize”按钮，用以将用户的非形式化表述自动转化为 Lean 的形式化语句。下方展示了一个 Lean 代码编辑区域，用户可在此查看并手动修订自动生成、以 by sorry 结尾的定理声明。界面底部并排放置了“Generate Proof”和“Use pass@16”两枚操作按钮（语言模型常用的 pass@N——给定 N 次尝试，若任意一次成功即计为通过）。

---

建议在开始之前，先使用语义搜索引擎 leansearch.net在mathlib4中查询相关定理，避免重复造轮子

hbghlyj

Lagrange插值定理：给定 $n$ 个两两不同的实数 $x_1,\dots,x_n$ 及任意实数 $y_1,\dots,y_n$，有且仅有一个次数 $<n$ 的多项式 $P$，满足 $\forall i$ 有 $P(x_i)=y_i$.

我撰写了page/linear algebra/Lagrange interpolation点击右上角按钮，在线运行Lean，光标移到文件末，看到No goals消息，所以证明是正确的。但是，由于不熟悉Lean，我写得极其冗长，希望得到简化

思路

令 $V$ 为次数小于 $n$ 的实系数多项式的空间，令 $W$ 为从指标集 $\mathrm{Fin}\, (n+1)$ 到 $\mathbb{R}$ 的函数空间；二者都是维数为 $n$ 的实向量空间。构造线性映射
$$
T:V\to W,\quad p\mapsto\bigl(i\mapsto p.\mathrm{eval}(x_i)\bigr),
$$
并证明其单射，结合维数相等的事实，由injective_iff_surjective_of_finrank_eq_finrank推出 $T$ 也必定是满射，从而得到插值多项式的存在性；单射性又保证了该多项式的唯一性。

hbghlyj

page/linear algebra/diagonalizable
这里有一些更难的证明，如何用Lean写出