build: remove lean4checker

[stephen-huan]

lean4checker is deprecated and can be replaced with Lean.Replay from the Lean repository.

Passes lean --run runtests.lean with actual landrun on Linux. Tested on Lean (version 4.29.1, commit v4.29.1, Release) from NixOS. The elan toolchain gives me the following error which I haven't tracked down yet.

[landrun:error] 2026/06/04 03:15:15 Failed to detect library dependencies: exit status 1
uncaught exception: Child exited with 1

(almost surely a nixos issue, e.g. I get [landrun:error] 2026/06/04 03:16:18 Failed to detect library dependencies: fork/exec /nix/store/pf30k3mg7n6bibc1k6609gyq7glk00k2-glibc-2.42-61-bin/bin/ldd: no such file or directory with no /bin/sh. These changes should not depend on the toolchain as long as it's past 4.28.0)

[stephen-huan]

Small nit, but if you actually run the instructions then you'll create a .lake directory in tests/projects/simple_mismatch. The current .gitignore only ignores .lake at the root.

[stephen-huan]

Hmm, it seems to break pattern matching. If I have the following Challenge.lean and Solution.lean,

def is_even : Nat -> Bool
  | 0 => true
  | 1 => false
  | n + 2 => is_even n
termination_by structural n => n

theorem test {n : Nat} (h : ∃ k, n = 2 * k) : is_even n = true :=
  sorry

def is_even : Nat -> Bool
  | 0 => true
  | 1 => false
  | n + 2 => is_even n
termination_by structural n => n

theorem test {n : Nat} (h : ∃ k, n = 2 * k) : is_even n = true := by
  fun_induction is_even with
  | case1 => decide
  | case2 => omega
  | case3 n ih => match h with
    | ⟨k, _⟩ => exact ih ⟨k - 1, by omega⟩

Then I get the following error.

Building Challenge
⚠ [2/3] Built Challenge
warning: Challenge.lean:7:8: declaration uses `sorry`
Build completed successfully (3 jobs).
Exporting #[test, propext, Quot.sound, Classical.choice, Nat.add, Nat.sub, Nat.mul, Nat.pow, Nat.gcd, Nat.div, Nat.mod, Nat.beq, Nat.ble, Nat.land, Nat.lor, Nat.xor, Nat.shiftLeft, Nat.shiftRight, String.ofList] from Challenge
Building Solution
Build completed successfully (3 jobs).
Exporting #[test, propext, Quot.sound, Classical.choice, Nat.add, Nat.sub, Nat.mul, Nat.pow, Nat.gcd, Nat.div, Nat.mod, Nat.beq, Nat.ble, Nat.land, Nat.lor, Nat.xor, Nat.shiftLeft, Nat.shiftRight, String.ofList] from Solution
Running Lean default kernel on solution.
uncaught exception: No such recursor Lean.Syntax.rec_2