Proof index Open problems Projects Researchers Packages MCP

Search Lean proofs

Sign in Sign up

Open navigation

Search Lean proofs

Proof index Open problems Research projects Researchers Lean packages Connect MCP Search Mathlib Check Lean code

Research proofs Open problems Mathlib Type and shape search

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

Search proofs

1 topic

Search topics

ABC conjectureabstractabstract lang completenessactionadditive combinatoricsadele ringadic valuationaffine groupaffine spacesahiv22ahiv22supportalgebraic geometryalgorithmallow denyallows termalmost orthogonalityalmost periodicityanalysisanalytic number theoryanalytic setangular momentumangular velocityantichain operatorantichain tile countappendapprox hom pfrapproximationarcaritharithmetic geometryarithmetic progressionsas tensorasymptoticsasync runtimeauthorizationauthorizeauthorizerautomata theoryautomorphismauxiliaryball extensionball scalingbase changebase permbasicbasicsbasisbasis linearbatched evaluatorbehavioural theoryberlekamp welchbig opbijectivitybilinear formbindingbirthdaybisimulationbivariateblock rel distancebmobn254borel caratheodorybounding mutualbraketbridgebrownian motionbrun titchmarshbuchi congrbuchi congruencebuchi interbundledbundled semanticscaching logging oraclecaching oraclecadlagcadlag modificationcalculationscampanatocan reach viacanonicalcapacitycardinalitycarleson huntcarleson hunt basiccarleson on the real line basiccarleson on the real line continuouscarleson operator realcategory theorycell refchainchangcheck claimchernoffchiral indiceschoueka lemmachurchclass dclass field theoryclassical carlesonclifford algebracma to nmaco psetcoding theorycollisioncollision resistancecombinatoricscombinecommutationcommutative algebracompactcompact hausdorff ringscompact systemcompatibilitycompiled policiescompilercompletenesscompletionscomplexity theorycompositioncomputabilitycomputer scienceconcatconclusionsconcretecondconfluencecongrconsensusconsequencesconsistencyconstantconstant slice distconstant time distconstructionscontinuitycontractioncontractionscontrol approximation effectcontrol approximation effect basiccontrol approximation effect continuousconversionconvolutioncoordinatecore interaction phasecorrectnesscorrugationcostcost accountingcost modelcounter modelcovariancecross productcryptographycurlcutoff admissibilitycyclotomic fieldsdebutdecoderdecoding radiusdedekind mac neille completiondeferred samplingdefsdegree conflictdeltaderivativederivativesdetdet concatdet muller langdetailsdeterministicdifferential geometrydiffie hellmanDiophantine equationsdirichlet kerneldisagreementdiscretedist equivdist of functiondistancedistributiondivdivergence of setsdomaindoob lpdoob meyerdoubling measuredown singletdpidrcdualdual pairdyn systeme2eagereager tableeffective potentialeigenfunctioneisensteineisenstein asymptoticselectric fieldelliptic coefficientsembeddingempotentialendgameenergyenforcementenforcerensembleentanglemententropyentropy pfrequation1323equation677equational logicestimateeuler lagrangeeuler maclaurineuler mascheroni boundseval disteval splitevaluationevaluation binding conflictevaluatorexamplesexceptional setexecutionexistenceexistence theoryexpected costexponential integrabilityexponential mapextractabilityextractorfactorizationfair schedulerFermat's Last Theoremfgfibringfidelityfieldfield strengthfinitary carlesonfinitefinite adele ringfinite coverfinite dimensionalfinite fieldfinitenessfinset termsfirstfirst estimatefive quantaflattenflex approxfoldingfolding polynomialforest complementforest unionforestsforkformal languagesformal logicfoundationsfourierFourier analysisfree semigroupfree statefrey packagefrobeniusfrom mathlibfrom unaryfull beta confluencefull beta eta confluencefull etafunctiongadgetsgauge transformationgen heapgen setsgeneralgeneralizedgenerate seedgeneric liftghost mapgradgradinggrid structuregromovgroupgroup theory stuffguruswamiguruswami sudanhaltinghamiltonianhandler from unaryhandler specsharmonic analysisharmonic waveharnackhas tauhas var adjointhash commitmentheat kernelheat solutionheat solution propertyhelperherbrand quotienthilbert kernelhilbert strong typehilbert94histholder normholder van der corputhom pfrhomotopyhopshprinciplehundred percenthypothesis testingideal gasidentical until badimmersionimplimplicationsimproved pfrindicatorinduction scheme delta1inductive constructionsinequalitiesinf modelinf occinfinite graph ramseyinfinite wireinflationinputinsert and contractinsert and contract natinsert noneinsert someinsertion sortinstanceinstancesintegralintegral closureinteractive protocolsinterleaved codeintervalinverse iterationis dist boundedis extremais plane waveis viableisqbridgeiteriterated laplacianiterationiwaniec kowalski ch1kemdemkey encap mechkinetic energykinetic termknowledge soundnesskoszul signkullbackkummers lemmal2estimatelagrangianlanguagelaplace inversionlaplace runge lenz vectorlarge separationleakagelemmaslevelslex'orderlie traceline in cubiclinear codelinear mv extensionlinearizedlinftylipschitz normlistlocallocal fieldslocal john nirenberglocalisation datalocallyloglog gradientlogging oraclelooplp function toolkitls corelyubashevsky seilermac from prfmachinemagnetic fieldmainmain resultsmain theoremmain thmmapmap unionmarcinkiewicz zygmundmatrix derivativesmatrix divmatrix mapmaximal inequalitymcageneratormdifferentiablemdscodemeasure theorymedium pntmellin calculusmetatheorymetricmicciancio youngmin layer tilesminimal super setmllmodel datamodular formsmodulemodulesmomentummon predmore ruzsa distmotionmstatemulti appmulti tau functionalmultilinearmultiplicationmyhill nerodenavier stokesnegligibleno entities errornon deterministicnontangential operatornormnorm boundnorm pownormal ordernormsnumber theoryobelixobservation oracleof envof finsetof potential termofeoi2omega executionomega languageomega reg langomega regular languageone dimensionone jet bundleoperatorsopsoptoptionoptional samplingoracleorderpackingpadicpairparameterizationparametric hprinciplepartial differential equationspartial mapperfect secrecypermutative extensionperron formulapheno closedpheno constrainedphi transformphys hermitephysicspick subsetpinchingpmfpointwise estimatepolicypolicy slicepolynomialpositionpositive partpositive part preludepotentialprepre estimatepre iterationprelimspreludepreserves invpreserves type ofprime numbersprimrec codingprobabilityprobe epsprodproductprogram logicprogram semanticsprogram verificationprogramming oracleproof dataproof systemsproof theoryproperpropertiesproximity generatorspsetpsipublic estimateqpquadratic twistsquantative estimatequantitativequantum channelsquantum field theoryquantum informationquark doubletquery boundquicksortquotientradial angular measureramanujan identitiesrandom queryrational functionsreachablereal complexrectanglerectangle argument principlerecurrencerecursionreduce claimreductionreduction base changereductionsreed solomonrefutabilityreg langregular languageregularity theoryregularizedregularized energyregularized witnessesreindexingrelrelationrelationsrelativerelative distancerelativityremaining tilesreparametrizationreplay forkres to imag axisresidualresidue calc on rectanglesresolventresource profileresponderrestrict degreerestrict degree varrestricted provabilityrestricted weak typerestrictionresultantresultsrho functionalrough inputround consistencyrowsrqrudinsafetysampleable typesamplingscaled ball estimatesschur triangulationschwartz submoduleschwartz zippel countingsec expsecond estimatesection2section4securityseeded forkseeded oraclesegmentself adjointsemanticssend challengesend claimsend witnessseparation logicseq composeserre approximationserre derivative slashsetset theoryshamirsigmasignature algsimple processsimulate qsimulationsinc kernel error boundssingle roundslash action auxilslicesmooth approximationsmooth embeddingsmooth existencesmooth testssobolevsobolev poincaresobolev spacessolid spheresolutionsoundnessspectral projection boundsphere packingsplit foldsplit multiplicative reductionsplitting modulesquare integrablessastage onestampacchia truncationstandard formstandard reductionstate projectionstate separatingstatementstatic contractstatic wick termstd do bridgestepsstochastic intervalstochastic processesstr actionstraight linestrong normstrong pntstructuressub specsubdomainsubtypesucc succ abovesumsumcheck phasesuper commutesupportsurroundingsymbolic compilationsymbolizersymm enc algsymmetrictake droptanhtate curvetate curve base changetate curve constructiontate parametertau functionaltau in queriesten quantatensor producttensorialtest functionsthermo quantitiesthree apthree dimensiontile correlationtile existencetile structuretime contracttime contractiontime liketime ordertime slicetiseto complexto fft domainto nato singleto single acceptto solstopologytorsion endgametotaltotal derivative equivalencetpetracetrace inner producttrace vanishingtrajectorytraversaltrivial cohomologytriviality criteriontruncationttransformtvdisttwotwo statetypecheckertypecheckingtypingudfultraproductunaryunbalancingunboundedunbundleduncertaintyuncontracted listuniform integrableuniquenessunitunit tensorunitaryuniversal algebraunpredictabilityunramifiedup downup singletupdatesutransformvalid refsvalidationvan der corputvandermondevariancevcdimensionvector bundlesverificationverifierversion spaceversion space latticeweak calderon zygmundweak derivativeweak derivativesweak harnackweak pfrweightedweighted estimateswell typedwell typed okwell typed verificationwfwhole space sobolevwick contractionswick termwicks theorem normalwienerwired runwith abortwitnesseswriter costyukawazero consensuszero count crudezeta boundszf

Source projectLean version

2 results

Project-declaredLean 4.31.0

Typecheck is sound

Cedar.Thm.typecheck_is_sound

Plain-language statement

If typechecking succeeds, then for any request consistent with the schema, either (1) evaluation produces a boolean or (2) it returns an error of type entityDoesNotExist, extensionError, or arithBoundsError. Both options are encoded in the EvaluatesTo predicate. The type checker cannot protect against these errors because it has no knowledge of th...

authorizationprogram verificationsemantics

Source project: Cedar Specification

Person-level attribution pending.

View proof record

Project-declaredLean 4.31.0

Typechecked is well typed after lifting

Cedar.Thm.typechecked_is_well_typed_after_lifting

Plain-language statement

The type checker produces typed expressions that are well-typed after type lifting. TODO: move this around after the proof is fixed

authorizationprogram verificationsemantics

Source project: Cedar Specification

Person-level attribution pending.

View proof record

Search complete Lean declarations, inspect their provenance, and check code in a live Lean environment.

Research

Research proofs Open problems Search Mathlib Type and shape search Projects Researchers

Use Therefore

Check a proof Packages MCP, API, and editor Verification model

Built for the Lean community.Verification, provenance, and authorship stay separate.