Skip to main content

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

Showing 1,927 to 1,932 of 2,569 results.

Project-declaredLean 4.32.0

Prf implies uf cma

PRFScheme.prf_implies_uf_cma

Mathematical statement

Boneh-Shoup Theorem 6.2. PRF security implies UF-CMA security for the derived MAC: for any forger A, the constructed distinguisher macToPRFReduction prf A satisfies UF_CMA_Advantage(A) ≤ prfAdvantage(prf, B) + 1/|R|.

program verificationseparation logiccryptography

Source project: VCVio

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Prf Ideal Exp mac To PRFReduction le

PRFScheme.prfIdealExp_macToPRFReduction_le

Mathematical statement

In the ideal PRF experiment (random oracle), the reduction succeeds with probability at most 1/|R| , a fresh random oracle query is independent of the forger's output.

program verificationseparation logiccryptography

Source project: VCVio

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Prime between

prime_between

Mathematical statement

For every ε>0\varepsilon>0, every sufficiently large real number xx has a prime pp in the short multiplicative interval x<p<(1+ε)xx<p<(1+\varepsilon)x.

analytic number theoryprime numbersasymptotics

Source project: Prime Number Theorem and More

Person-level attribution pending.

View proof record
Project-declaredLean 4.31.0

Prob eval zero le div

prob_eval_zero_le_div

Mathematical statement

Probability of a nonzero polynomial evaluating to zero over a uniform product distribution is at most d / m, where d bounds the total degree and m bounds below the cardinality of each factor. This bridges schwartz_zippel_counting with the probability formulation.

cryptographyproof systemscoding theory

Source project: ArkLib

Person-level attribution pending.

View proof record
Project-declaredLean 4.31.0

Prob marginalization first of prod

prob_marginalization_first_of_prod

Project documentation

Helper lemma for probability marginalization. Pr_{ (x, y) ← D₁ × D₂ }[ P x ] = Pr_{ x ← D₁ }[ P x ]

cryptographyproof systemscoding theory

Source project: ArkLib

Person-level attribution pending.

View proof record
Project-declaredLean 4.31.0

Prob schwartz zippel mv polynomial

prob_schwartz_zippel_mv_polynomial

Mathematical statement

Schwartz-Zippel Lemma (Probability Form): For a non-zero multivariate polynomial P of total degree at most d over a finite field L, the probability that P(r) evaluates to 0 for a uniformly random r is at most d / |L|.

cryptographyproof systemscoding theory

Source project: ArkLib

Person-level attribution pending.

View proof record