Lean repository linked
Quantitative concatenation for polynomial box norms
arXiv:2407.08636 · arXiv
Lean formalisations (1)
cadamcat/hindman-sums-products-lean4 at 09b8fde6e5cd
Linked by the repository’s formalization.yaml.
Project review: agent-reviewed
Audit: awaiting publication.