Vibe formalization of sum-check

SumcheckExperiment/Basic.lean contains a vibe formalization of sumcheck, maybe. I still need to read it.

What I did

I asked Claude Code (Opus 4.6)

Please create a single-file LaTeX document that describes the sum-check protocol in a modern way. Please cite the relevant documents. This file will be a formalization target, so clear definitions and statements and proofs will be appreciated.

The result is in docs directory.

I asked Aristotle to formalize the LaTeX document repeatedly. When Aristotle was not producing new code, I asked Claude Code to state the missing theorem, and asked Aristotle to finish the proofs.

What I have not done

I have not examined the LaTeX document or the Lean definitions or statements in detail.