lean-checker: A Lean 4 + Mathlib Verification Service

Read full text
Authors: Andrey P. Khalov, Olga M. Ataeva, Natalia P. Tuchkova
Cited by: 2

Abstract

A Dockerized FastAPI service that verifies Lean 4 source code inside a pinned Mathlib environment and returns structured JSON diagnostics with error coordinates.

Publication details

Journal / source
Zenodo (CERN European Organization for Nuclear Research)
Publication date
5 May 2026
Language
EN