Source-pinned research

Research proof index

Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.

This index contains 2,569 research declarations. Search 10,000 more complete Mathlib declarations.

All topics

2569 results

Project-declaredLean 4.33.0-rc1

Better PFR conjecture

better_PFR_conjecture

Plain-language statement

If AF2nA \subset {\bf F}_2^n is finite non-empty with A+AKA|A+A| \leq K|A|, then there exists a subgroup HH of F2n{\bf F}_2^n with HA|H| \leq |A| such that AA can be covered by at most 2K92K^9 translates of HH.

additive combinatoricsentropyprobability

Source project: Polynomial Freiman-Ruzsa project

Person-level attribution pending.

View proof record
Project-declaredLean 4.33.0-rc1

Better PFR conjecture

better_PFR_conjecture'

Project documentation

Polynomial Freiman-Ruzsa theorem with exponent 99, without a finite ambient-group assumption. Let AA be a nonempty finite subset of an elementary abelian 22-group. If A+AKA|A+A|\le K|A|, then there are a finite subspace HH and a finite set cc such that Ac+HA\subseteq c+H, c<2K9|c|<2K^9, and HA|H|\le|A|.

additive combinatoricsentropyprobability

Source project: Polynomial Freiman-Ruzsa project

Person-level attribution pending.

View proof record
Project-declaredLean 4.31.0

Commit Oracle Verifier rbr Knowledge Soundness

Binius.BinaryBasefold.CoreInteraction.commitOracleVerifier_rbrKnowledgeSoundness

Plain-language statement

RBR knowledge soundness for a single round oracle verifier

cryptographyproof systemscoding theory

Source project: ArkLib

Person-level attribution pending.

View proof record