Lean 4 Kernel Type Checker in Pascal

The Lean 4 kernel is the small trusted core of a major proof assistant: a dependent type theory with universes, inductive families, recursors, quotient types, and definitional equality (everything Mathlib's formalized mathematics ultimately rests on). Independent kernel re-implementations exist precisely so the kernel can be cross-checked, and this task asks for one: a standalone checker that reads exported Lean environments and decides, declaration by declaration, whether they are admissible.

The difficulty is twofold. Semantically, the checker must reproduce subtle kernel behavior: reduction, universe handling, the Nat and String literal extensions, and the admissibility rules for (possibly mutual and nested) inductives. Operationally, real inputs are large: exports range from a few hundred bytes to about 90 MB with over 1.5 million objects, so throughput is part of what is measured.

Implement the Lean 4 kernel's type checker in the Free Pascal project at /app/checker/, with sources only as Pascal files under src/ and the program entry in src/checker.pas. The documented fpc build line produces build/checker, invoked as checker <path-to-export-file>.

• Exit 0 if and only if every declaration in the lean4export NDJSON file is well-formed, well-typed and admissible, and the file is structurally valid; exit non-zero otherwise. The exit code is the result.
• Never exit 0 on an input the checker failed to understand (an unparsed construct or an internal error is not evidence of admissibility), and never reject a file merely because it is expensive.
• Soundness is paramount: wrongly certifying an environment that derives a closed proof of False is the most serious error the checker can make.
• Decide everything in Pascal itself, the way the Lean kernel would: the checker must be a self-contained static binary.

/app/README.md carries the CLI contract, the complete NDJSON wire-format specification (names, levels, expressions, and all six declaration kinds, adapted from lean4export's format document), and the build and test commands. /app/exports/ holds worked examples of both verdicts (every file under accept/ must exit 0 and every file under reject/ must not, with expected.tsv listing them all), and /app/run-tests.sh builds the checker and runs any subset. The Free Pascal compiler is preinstalled and the machine is offline.

A clean-room verifier, separate from the agent's environment, stages only the Pascal sources under src/, rebuilds them offline with fpc -O2as a non-root user, and runs a hidden corpus of 607 export files (~2.4 GB): genuine Lean, Mathlib, Batteries and Aesop environments to accept, plus 131 deliberately corrupted or False-grafted exports to reject, each labeled offline by an independent reference kernel (nanoda_lib). Cases are staged under content-hash names with uniform timestamps, so neither path nor order reveals a verdict; the checker's exit status on each file is the verdict.

• Reward is the weighted accept rate times the weighted reject rate, with soundness-tier cases weighted 10×. Exiting 0 on any case containing a closed proof of False is a hard zero.
• A static anti-delegation scan (process-spawning APIs, dynamic loading, spawn-shaped FFI declarations) plus a runtime exec tripwire zero the result if the checker hands the decision to another program.
• Each case gets a size-scaled budget (15 s plus ~1.2 MB per second, about 10× the reference kernel's throughput) inside a 2400-second suite budget; a crash, hang, timeout or unreached case counts as a wrong verdict, never a skip.
• Build failures (600-second cap) and a missing src/checker.pas entry point zero the result.