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.30.0

Swap xx heat Kernel

swap_xx_heatKernel

Plain-language statement

Swap the second spatial derivative xx\partial_{xx} with the integral \int.

partial differential equationsSobolev spacesanalysis

Source project: PDE

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Cipher Given Msg uniform of uniform Key of unique Key

SymmEncAlg.cipherGivenMsg_uniform_of_uniformKey_of_uniqueKey

Project documentation

Core uniformity lemma: uniform keygen plus unique key per (message, ciphertext) pair implies every (message, ciphertext) conditional has probability (card K)⁻¹. Both Shannon theorems follow from this.

program verificationseparation logiccryptography

Source project: VCVio

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Perfect Secrecy At of uniform Key of unique Key

SymmEncAlg.perfectSecrecyAt_of_uniformKey_of_uniqueKey

Plain-language statement

Constructive Shannon direction: if keygen is uniform and each (message, ciphertext) pair is realized by a unique key in support, then perfect secrecy holds. deterministicEnc asserts encryption is deterministic in distribution (singleton support for each fixed (key, message)).

program verificationseparation logiccryptography

Source project: VCVio

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Analytic weierstrass

TateCurve.Blueprint.analytic_weierstrass

Project documentation

The analytic form of the main theorem (Silverman, Advanced topics, Theorem V.1.1(a)): for 0 < ‖q‖ < ‖u‖ < 1, Yₐ² + XₐYₐ = Xₐ³ - 5s₃(q)Xₐ - (5s₃(q) + 7s₅(q))/12. Proof sketch: the hypotheses ensure u ∉ qᶻ, and we may choose z, τ with e z = u, e τ = q, 0 < im z < im τ (so z ∉ Λ_τ). Substitute the four q-expansions into the differential...

number theoryarithmetic geometryFermat's Last Theorem

Source project: Fermat's Last Theorem

Person-level attribution pending.

View proof record