Source-pinned research
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.
2569 results
Binius.FRIBinius.CoreInteractionPhase.coreInteractionOracleVerifier_rbrKnowledgeSoundness
Plain-language statement
Round-by-round knowledge soundness for the core interaction oracle verifier
Source project: ArkLib
Person-level attribution pending.
BlockRelDistance.listBlock_subset_listHamming
Plain-language statement
Claim 4.19 from [ACFY24], Part 2 As a consequence of relHammingDist_le_blockRelDistance, the list of codewords within a certain block relative distance δ is a subset of the list of codewords within the same relative Hamming distance δ.
Source project: ArkLib
Person-level attribution pending.
BlockRelDistance.relHammingDist_le_blockRelDistance
Plain-language statement
Claim 4.19 from [ACFY24], Part 1 For a smooth Reed-Solomon code, the standard relative Hamming distance δᵣ(f,g) is a lower bound for the k-wise block relative distance δᵣ(k, φ, f, g).
Source project: ArkLib
Person-level attribution pending.
BN254.BaseField_is_prime
Plain-language statement
Proof that the BN254 base field characteristic is prime
Source project: ArkLib
Person-level attribution pending.
bob_complete
Plain-language statement
Honest Bob usually accepts if Alice is off by ≤ c
Source project: debate
Person-level attribution pending.
bob_debate_cost
Plain-language statement
Bob makes few queries, regardless of Alice and Vera
Source project: debate
Person-level attribution pending.