SCP

Attempt at formalising split conformal prediction in Lean4. Many thanks to everyone from formalising mathematics.

Usage

nix develop

You should now have Lean and Lake pointing to the right toolchain and about 6 GiB of local cache in local .lake directory. Mind the first run on a fresh clone takes a while to fetch. Your editor may now be able to use Lean directly via LSP. For example, I use nvim with lean.nvim. To interact with the proof

nvim SCP/FM1/Project.lean

To build everything without an editor

lake build SCP

To build report(s)

tectonic SCP/FM1/report.tex