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 573 research declarations. Search 10,000 more complete Mathlib declarations.

1 topic

573 results

Clear filters
Project-declaredLean 4.31.0

Schwartz zippel counting

schwartz_zippel_counting

Plain-language statement

For a nonzero multivariate polynomial f of total degree at most d, evaluated over a product of finite subsets of a field F, each of cardinality at least m, the number of roots is at most d / m multiplied by the side of the product set.

cryptographyproof systemscoding theory

Source project: ArkLib

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Eval Dist lift Comp generate Seed bind simulate Q run' take At Index

seededOracle.evalDist_liftComp_generateSeed_bind_simulateQ_run'_takeAtIndex

Plain-language statement

Truncating the seed at oracle i₀ to only the first k entries does not change the distribution when averaging over seeds from generateSeed.

program verificationseparation logiccryptography

Source project: VCVio

Person-level attribution pending.

View proof record
Project-declaredLean 4.31.0

Oracle Verifier to Verifier run

SendChallenge.oracleVerifier_toVerifier_run

Plain-language statement

The pure verifier's underlying non-oracle verifier returns the statement together with the sampled challenge (read off the transcript), with the oracle statements passed through.

cryptographyproof systemscoding theory

Source project: ArkLib

Person-level attribution pending.

View proof record
Project-declaredLean 4.31.0

Oracle Verifier coordinate Wise Special Sound

SendClaim.oracleVerifier_coordinateWiseSpecialSound

Project documentation

Coordinate-wise special soundness of SendClaim. The verifier is a pure pass-through with no challenge rounds, so CWSS collapses (via the oracle no-challenge bridge) to a transcript-level obligation. The extractor is trivial (e := fun _ _ => (), there is no witness); since the output oracle statements at inl are the input oracles unchanged and `t...

cryptographyproof systemscoding theory

Source project: ArkLib

Person-level attribution pending.

View proof record
Project-declaredLean 4.31.0

Oracle Verifier to Verifier run

SendClaim.oracleVerifier_toVerifier_run

Plain-language statement

The pure pass-through oracle verifier's underlying non-oracle verifier returns the statement together with the output oracle statements (input oracles at inl, the message at inr 0).

cryptographyproof systemscoding theory

Source project: ArkLib

Person-level attribution pending.

View proof record
Project-declaredLean 4.31.0

Oracle Verifier coordinate Wise Special Sound

SendSingleWitness.oracleVerifier_coordinateWiseSpecialSound

Project documentation

Coordinate-wise special soundness of SendSingleWitness. The oracle verifier has no challenge rounds, so CWSS collapses (via the oracle no-challenge bridge coordinateWiseSpecialSound_of_isEmpty_challengeIdx) to a transcript-level extraction obligation on the combined statement Statement × (∀ i, OStatement i). The extractor is `e := fun _ tr => tr...

cryptographyproof systemscoding theory

Source project: ArkLib

Person-level attribution pending.

View proof record