anthropics/formal-math
File Size
The distribution of size of files (measured in lines of code).
File Size Overall
  • There are 769 files with 183,419 lines of code.
    • 12 very long files (21,098 lines of code)
    • 55 long files (34,966 lines of code)
    • 263 medium size files (81,906 lines of code)
    • 231 small files (33,309 lines of code)
    • 208 very small files (12,140 lines of code)
11% | 19% | 44% | 18% | 6%
Legend:
1001+
501-1000
201-500
101-200
1-100


explore: grouped by folders | grouped by size | sunburst | 3D view
File Size per Extension
1001+
501-1000
201-500
101-200
1-100
lean11% | 19% | 44% | 18% | 6%
py0% | 0% | 66% | 24% | 8%
yaml0% | 0% | 97% | 0% | 2%
rb0% | 0% | 0% | 100% | 0%
toml0% | 0% | 0% | 0% | 100%
File Size per Logical Decomposition
primary
1001+
501-1000
201-500
101-200
1-100
zeta2318% | 24% | 38% | 13% | 4%
3sum-apsp3% | 12% | 51% | 23% | 8%
.github0% | 0% | 0% | 0% | 100%
Longest Files (Top 50)
File# lines# units
lean
 3474 -
lean
MediumPNT.lean
in zeta23/Zeta23/FromPNTPlus
 3387 -
lean
ZetaBounds.lean
in zeta23/Zeta23/FromPNTPlus
 2788 -
lean
Window.lean
in zeta23/Zeta23/ThmD
 1737 -
lean
Assembly.lean
in zeta23/Zeta23
 1451 -
lean
PrimeSideChi.lean
in zeta23/Zeta23/ThmE
 1381 -
lean
ZeroFree.lean
in zeta23/Zeta23/XiPrime/ExplicitFormula
 1351 -
lean
Basic.lean
in zeta23/Zeta23/PrimeSideA
 1276 -
lean
Chebyshev.lean
in zeta23/Zeta23
 1144 -
lean
ResidueCalcOnRectangles.lean
in zeta23/Zeta23/FromPNTPlus
 1062 -
lean
Expansion.lean
in zeta23/Zeta23/XiPrime/ExplicitFormula
 1035 -
lean
TestWeight.lean
in zeta23/Zeta23/XiPrime/ExplicitFormula
 1012 -
lean
Transfer.lean
in zeta23/Zeta23/XiPrime
 982 -
lean
MellinCalculus.lean
in zeta23/Zeta23/FromPNTPlus
 974 -
lean
PPChi.lean
in zeta23/Zeta23/ThmE
 946 -
lean
Effective.lean
in zeta23/Zeta23/WeilEF
 909 -
lean
Decay.lean
in zeta23/Zeta23/Taper
 908 -
lean
EndsE1.lean
in zeta23/Zeta23/PrimeSideA
 851 -
lean
ZeroSide.lean
in zeta23/Zeta23
 830 -
lean
EndsNu.lean
in zeta23/Zeta23/PrimeSideA
 768 -
lean
VerticalLine.lean
in zeta23/Zeta23/WeilEF
 763 -
lean
PrimeSideB.lean
in zeta23/Zeta23
 746 -
lean
NodeArray.lean
in 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe
 740 -
lean
Host.lean
in 3sum-apsp/ThreeSumApsp/Programs/Sec5/Corollary39/MinMaxWeight
 714 -
lean
AllPairs.lean
in 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21b/MinPlus
 704 -
lean
BandArray.lean
in 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/Encode
 669 -
lean
ExplicitFormula.lean
in zeta23/Zeta23
 662 -
lean
EFExpansion.lean
in zeta23/Zeta23/XiPrime/Hardy
 650 -
lean
PPKernel.lean
in zeta23/Zeta23/PrimeSideB
 642 -
lean
IntMuChi.lean
in zeta23/Zeta23/ThmE
 641 -
lean
Landau.lean
in zeta23/Zeta23/WeilEF
 641 -
lean
Traces.lean
in zeta23/Zeta23/ThmD
 640 -
lean
Codes.lean
in 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/Wanted
 633 -
lean
Nodes.lean
in 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe
 620 -
lean
Tail.lean
in zeta23/Zeta23
 615 -
lean
Strassen.lean
in 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Hashing
 615 -
lean
FullLineChiProof.lean
in zeta23/Zeta23/ThmE
 613 -
lean
Buckets.lean
in 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe
 608 -
lean
PP.lean
in zeta23/Zeta23/XiPrime/PrimeSide
 605 -
lean
EndsCore.lean
in zeta23/Zeta23/PrimeSideA
 604 -
lean
SharedStage.lean
in 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5
 601 -
lean
MaxTriangle.lean
in 3sum-apsp/ThreeSumApsp/Programs/Sec5/Corollary39/MinMaxWeight
 597 -
lean
StirlingVert.lean
in zeta23/Zeta23/GammaFacts
 581 -
lean
Loop.lean
in 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Host
 580 -
lean
Host.lean
in 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21b/NegativeTriangle
 580 -
lean
Norms.lean
in zeta23/Zeta23/Taper
 577 -
lean
Reduction.lean
in 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe
 574 -
lean
Dependence.lean
in zeta23/Zeta23/XiPrime/Transfer
 565 -
lean
Modulus.lean
in 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe
 565 -
lean
Generic.lean
in zeta23/Zeta23/XiPrime/ZeroCount
 556 -
Large Files That Change Often (Top 20)
To change a file, an AI coding agent (or a person) has to read it: these files are read the most for the changes in the past year (lines × changes).
File# lines≈ tokens
to read		# changes
(1y)		≈ lines edited
per change		lines read per
line changed
lean
MediumPNT.lean
in zeta23/Zeta23/FromPNTPlus
 3387 ~20k–50k 2 ~3,000 ~1
lean
ZetaBounds.lean
in zeta23/Zeta23/FromPNTPlus
 2788 ~15k–50k 2 ~3,000 ~1
lean
 3474 ~20k–50k 1 ~5,000 ~1
lean
Window.lean
in zeta23/Zeta23/ThmD
 1737 ~10k–30k 2 ~2,000 ~1
lean
Assembly.lean
in zeta23/Zeta23
 1451 ~10k–30k 2 ~1,500 ~1
lean
PrimeSideChi.lean
in zeta23/Zeta23/ThmE
 1381 ~7k–20k 2 ~1,500 ~1
lean
ZeroFree.lean
in zeta23/Zeta23/XiPrime/ExplicitFormula
 1351 ~7k–20k 2 ~1,500 ~1
lean
Basic.lean
in zeta23/Zeta23/PrimeSideA
 1276 ~7k–20k 2 ~1,500 ~1
lean
Chebyshev.lean
in zeta23/Zeta23
 1144 ~7k–20k 2 ~1,000 ~1
lean
ResidueCalcOnRectangles.lean
in zeta23/Zeta23/FromPNTPlus
 1062 ~7k–15k 2 ~1,000 ~1
lean
Expansion.lean
in zeta23/Zeta23/XiPrime/ExplicitFormula
 1035 ~7k–15k 2 ~1,000 ~1
lean
TestWeight.lean
in zeta23/Zeta23/XiPrime/ExplicitFormula
 1012 ~7k–15k 2 ~1,000 ~1
lean
Transfer.lean
in zeta23/Zeta23/XiPrime
 982 ~5k–15k 2 ~1,000 ~1
lean
MellinCalculus.lean
in zeta23/Zeta23/FromPNTPlus
 974 ~5k–15k 2 ~1,000 ~1
lean
PPChi.lean
in zeta23/Zeta23/ThmE
 946 ~5k–15k 2 ~1,000 ~1
lean
Effective.lean
in zeta23/Zeta23/WeilEF
 909 ~5k–15k 2 ~1,000 ~1
lean
Decay.lean
in zeta23/Zeta23/Taper
 908 ~5k–15k 2 ~1,000 ~1
lean
EndsE1.lean
in zeta23/Zeta23/PrimeSideA
 851 ~5k–15k 2 ~1,000 ~1
lean
ZeroSide.lean
in zeta23/Zeta23
 830 ~5k–15k 2 ~1,000 ~1
lean
EndsNu.lean
in zeta23/Zeta23/PrimeSideA
 768 ~5k–15k 2 ~700 ~1

Tokens are lines × 7 to 14 (analysis.fileReadsForChanges). Lines edited per change are the file's lines added and deleted divided by its commits over the whole history. Agents read about 2,000 lines at a time: when a 17,000-line file was split into modules, the tokens an agent read for the same change fell by 83% (The Economic Benefit of Refactoring, 2026).

Files With Most Units (Top 3)
File# lines# units
index.py
in 3sum-apsp/scripts
 383 13
generate.py
in 3sum-apsp/scripts
 141 5
validate-formalization.rb
in zeta23/scripts
 157 4
Files With Long Lines (Top 50)

There are 70 files with lines longer than 120 characters. In total, there are 273 long lines.

File# lines# units# long lines
lean
NumericCert.lean
in zeta23/Zeta23/PairCeiling
 286 - 25
lean
MediumPNT.lean
in zeta23/Zeta23/FromPNTPlus
 3387 - 20
generate.py
in 3sum-apsp/scripts
 141 5 20
lean
StrongPNTPrefix.lean
in zeta23/Zeta23/FromPNTPlus
 459 - 18
lean
Final.lean
in zeta23/Zeta23/XiPrime
 516 - 13
index.py
in 3sum-apsp/scripts
 383 13 13
lean
Rectangle.lean
in zeta23/Zeta23/XiPrime/Hardy/EFContour
 400 - 9
lean
RankTraceMult.lean
in zeta23/Zeta23/ZeroSide
 386 - 8
lean
PPChi.lean
in zeta23/Zeta23/ThmE
 946 - 8
lean
ResidueCalcOnRectangles.lean
in zeta23/Zeta23/FromPNTPlus
 1062 - 8
lean
LawN256.lean
in zeta23/Zeta23/PairCeiling
 287 - 7
lean
NearCUE.lean
in zeta23/Zeta23/PairCeiling
 205 - 7
lean
Traces.lean
in zeta23/Zeta23/PrimeSideB
 193 - 6
lean
DiagLaw.lean
in zeta23/Zeta23/XiPrime/Coeff
 430 - 6
lean
TightMult.lean
in zeta23/Zeta23/ZeroSide
 103 - 6
lean
Signed.lean
in zeta23/Zeta23/PairCeiling
 104 - 6
lean
ZetaBounds.lean
in zeta23/Zeta23/FromPNTPlus
 2788 - 6
lean
Gevrey.lean
in zeta23/Zeta23/Taper
 381 - 5
lean
Bridge.lean
in zeta23/Zeta23/PairCeiling
 206 - 5
lean
RowCert.lean
in zeta23/Zeta23/PairCeiling
 150 - 5
lean
EFContour.lean
in zeta23/Zeta23/XiPrime/Hardy
 426 - 4
lean
ReexpansionGen.lean
in zeta23/Zeta23/XiPrime/Coeff
 296 - 4
lean
GenericRvM.lean
in zeta23/Zeta23/XiPrime/ZeroCount
 274 - 3
lean
Mult.lean
in zeta23/Zeta23/ZeroSide
 179 - 3
lean
CeilingLaw256.lean
in zeta23/Zeta23/PairCeiling
 64 - 3
lean
Count.lean
in zeta23/Zeta23/XiPrime/Hardy
 263 - 2
lean
EFExpansion.lean
in zeta23/Zeta23/XiPrime/Hardy
 650 - 2
lean
NonSquarefree.lean
in zeta23/Zeta23/XiPrime/Coeff
 522 - 2
lean
PrimeSums.lean
in zeta23/Zeta23/XiPrime/Coeff
 128 - 2
lean
ReexpansionW.lean
in zeta23/Zeta23/XiPrime/Coeff
 46 - 2
lean
XiEFAssembly.lean
in zeta23/Zeta23/XiPrime/ExplicitFormula
 266 - 2
lean
Mult.lean
in zeta23/Zeta23/ThmE
 322 - 2
lean
Ceiling.lean
in zeta23/Zeta23/PairCeiling
 61 - 2
lean
EulerMaclaurin.lean
in zeta23/Zeta23/FromPNTPlus
 80 - 2
lakefile.toml
in 3sum-apsp
 29 - 2
228 - 1
validate-formalization.rb
in zeta23/scripts
 157 4 1
lean
Traces.lean
in zeta23/Zeta23/ThmDE
 251 - 1
lean
GzGp.lean
in zeta23/Zeta23/Hypotheses
 130 - 1
lean
EFMain.lean
in zeta23/Zeta23/XiPrime/Hardy
 402 - 1
lean
EFWeights.lean
in zeta23/Zeta23/XiPrime/Hardy
 195 - 1
lean
GramBridgeW.lean
in zeta23/Zeta23/XiPrime/Hardy
 123 - 1
lean
Seam.lean
in zeta23/Zeta23/XiPrime/Hardy
 120 - 1
lean
Basic.lean
in zeta23/Zeta23/XiPrime/Coeff
 323 - 1
lean
Statement.lean
in zeta23/Zeta23/XiPrime
 340 - 1
lean
W.lean
in zeta23/Zeta23/XiPrime/Transfer
 337 - 1
lean
InputsW.lean
in zeta23/Zeta23/XiPrime/Transfer
 43 - 1
lean
ZeroSide.lean
in zeta23/Zeta23/XiPrime/QuarticWindow
 181 - 1
lean
Moments.lean
in zeta23/Zeta23/XiPrime/QuarticWindow
 505 - 1
lean
LitCorr.lean
in zeta23/Zeta23/XiPrime/ExplicitFormula
 314 - 1
Correlations

File Size vs. Commits (all time): 769 points

3sum-apsp/Challenge/EndStatement.lean x: 1 commits (all time) y: 71 lines of code 3sum-apsp/Challenge/PaperStatements.lean x: 1 commits (all time) y: 218 lines of code 3sum-apsp/EndStatement.lean x: 1 commits (all time) y: 115 lines of code 3sum-apsp/PaperStatements.lean x: 1 commits (all time) y: 3474 lines of code 3sum-apsp/Solution/EndStatement.lean x: 1 commits (all time) y: 8 lines of code 3sum-apsp/ThreeSumApsp.lean x: 1 commits (all time) y: 20 lines of code 3sum-apsp/ThreeSumApsp/ConditionalTimes/Corollary38.lean x: 1 commits (all time) y: 57 lines of code 3sum-apsp/ThreeSumApsp/ConditionalTimes/Definitions.lean x: 1 commits (all time) y: 307 lines of code 3sum-apsp/ThreeSumApsp/ConditionalTimes/Theorem34.lean x: 1 commits (all time) y: 150 lines of code 3sum-apsp/ThreeSumApsp/ConditionalTimes/Theorem35.lean x: 1 commits (all time) y: 177 lines of code 3sum-apsp/ThreeSumApsp/Lang/Calls.lean x: 1 commits (all time) y: 104 lines of code 3sum-apsp/ThreeSumApsp/Lang/Compiler/CallFrames.lean x: 1 commits (all time) y: 134 lines of code 3sum-apsp/ThreeSumApsp/Lang/Compiler/Cells.lean x: 1 commits (all time) y: 273 lines of code 3sum-apsp/ThreeSumApsp/Lang/Compiler/ProgramCode.lean x: 1 commits (all time) y: 202 lines of code 3sum-apsp/ThreeSumApsp/Lang/Compiler/Simulation.lean x: 1 commits (all time) y: 427 lines of code 3sum-apsp/ThreeSumApsp/Lang/Compiler/StatementCode.lean x: 1 commits (all time) y: 294 lines of code 3sum-apsp/ThreeSumApsp/Lang/Compiler/WholeProgram.lean x: 1 commits (all time) y: 229 lines of code 3sum-apsp/ThreeSumApsp/Lang/Frames.lean x: 1 commits (all time) y: 338 lines of code 3sum-apsp/ThreeSumApsp/Lang/Lib/Emod.lean x: 1 commits (all time) y: 240 lines of code 3sum-apsp/ThreeSumApsp/Lang/Lib/PowTable.lean x: 1 commits (all time) y: 95 lines of code 3sum-apsp/ThreeSumApsp/Lang/Lib/RadixPass.lean x: 1 commits (all time) y: 159 lines of code 3sum-apsp/ThreeSumApsp/Lang/Lib/Seg.lean x: 1 commits (all time) y: 186 lines of code 3sum-apsp/ThreeSumApsp/Lang/Lib/Sieve.lean x: 1 commits (all time) y: 371 lines of code 3sum-apsp/ThreeSumApsp/Lang/Rules.lean x: 1 commits (all time) y: 316 lines of code 3sum-apsp/ThreeSumApsp/Lang/ToMachine.lean x: 1 commits (all time) y: 346 lines of code 3sum-apsp/ThreeSumApsp/Machine/PolylogIsLittleO.lean x: 1 commits (all time) y: 50 lines of code 3sum-apsp/ThreeSumApsp/Machine/Realized.lean x: 1 commits (all time) y: 33 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/Contracts.lean x: 1 commits (all time) y: 502 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/Encode/BandArray.lean x: 1 commits (all time) y: 669 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/SharedStage.lean x: 1 commits (all time) y: 601 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/Time.lean x: 1 commits (all time) y: 286 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/Wanted/Codes.lean x: 1 commits (all time) y: 633 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Corollary15_16/Split.lean x: 1 commits (all time) y: 461 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Hashing/Strassen.lean x: 1 commits (all time) y: 615 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Hashing/ZOrder.lean x: 1 commits (all time) y: 481 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Host/InstanceFacts.lean x: 1 commits (all time) y: 402 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Host/Loop.lean x: 1 commits (all time) y: 580 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Host/Text.lean x: 1 commits (all time) y: 356 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Instances/WriteMatrices.lean x: 1 commits (all time) y: 536 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe/Bits.lean x: 1 commits (all time) y: 412 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe/Contracts.lean x: 1 commits (all time) y: 440 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe/Modulus.lean x: 1 commits (all time) y: 565 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe/NodeArray.lean x: 1 commits (all time) y: 740 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe/Nodes.lean x: 1 commits (all time) y: 620 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21b/Apsp/Host.lean x: 1 commits (all time) y: 255 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21b/MinPlus/AllPairs.lean x: 1 commits (all time) y: 704 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec4/Theorem30/QuerySum.lean x: 1 commits (all time) y: 390 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec5/Corollary39/MinMaxWeight/Host.lean x: 1 commits (all time) y: 714 lines of code 3sum-apsp/ThreeSumApsp/RunningTimes/Sec3/Corollary15_16/Layout.lean x: 1 commits (all time) y: 515 lines of code 3sum-apsp/ThreeSumApsp/Sec2/Lemma10.lean x: 1 commits (all time) y: 525 lines of code zeta23/Zeta23/LinAlg/HermitianPosPart.lean x: 3 commits (all time) y: 167 lines of code zeta23/Zeta23/LinAlg/Inertia.lean x: 3 commits (all time) y: 125 lines of code zeta23/Zeta23/LinAlg/PosIndex.lean x: 3 commits (all time) y: 103 lines of code zeta23/Zeta23/LinAlg/RankTrace.lean x: 3 commits (all time) y: 239 lines of code zeta23/Zeta23/LinAlg/Sylvester.lean x: 3 commits (all time) y: 282 lines of code zeta23/Zeta23/LinAlg/VonNeumann.lean x: 3 commits (all time) y: 181 lines of code zeta23/Zeta23/LinAlg/Weyl.lean x: 3 commits (all time) y: 123 lines of code zeta23/formalization.yaml x: 5 commits (all time) y: 228 lines of code .github/dependabot.yml x: 2 commits (all time) y: 6 lines of code zeta23/Challenge.lean x: 2 commits (all time) y: 188 lines of code zeta23/Challenge/XiPrime.lean x: 2 commits (all time) y: 86 lines of code zeta23/ChallengeDeps/XiPrime.lean x: 2 commits (all time) y: 32 lines of code zeta23/Solution.lean x: 2 commits (all time) y: 119 lines of code zeta23/Solution/XiPrime.lean x: 2 commits (all time) y: 45 lines of code zeta23/lakefile.toml x: 4 commits (all time) y: 25 lines of code zeta23/scripts/PrintAxioms/PairCeiling.lean x: 2 commits (all time) y: 20 lines of code zeta23/scripts/validate-formalization.rb x: 2 commits (all time) y: 157 lines of code zeta23/Zeta23/Analytic/RectangleLogDeriv.lean x: 2 commits (all time) y: 373 lines of code zeta23/Zeta23/Analytic/Stirling.lean x: 2 commits (all time) y: 272 lines of code zeta23/Zeta23/Assembly.lean x: 2 commits (all time) y: 1451 lines of code zeta23/Zeta23/Assembly/Inputs.lean x: 2 commits (all time) y: 59 lines of code zeta23/Zeta23/Chebyshev.lean x: 2 commits (all time) y: 1144 lines of code zeta23/Zeta23/Defs.lean x: 2 commits (all time) y: 252 lines of code zeta23/Zeta23/Defs/LeafIntegrals.lean x: 2 commits (all time) y: 196 lines of code zeta23/Zeta23/ExplicitFormula.lean x: 2 commits (all time) y: 662 lines of code zeta23/Zeta23/Final.lean x: 2 commits (all time) y: 299 lines of code zeta23/Zeta23/FinalMult.lean x: 2 commits (all time) y: 345 lines of code zeta23/Zeta23/FromPNTPlus/Auxiliary.lean x: 2 commits (all time) y: 73 lines of code zeta23/Zeta23/FromPNTPlus/MediumPNT.lean x: 2 commits (all time) y: 3387 lines of code zeta23/Zeta23/FromPNTPlus/MellinCalculus.lean x: 2 commits (all time) y: 974 lines of code zeta23/Zeta23/FromPNTPlus/Mertens.lean x: 2 commits (all time) y: 177 lines of code zeta23/Zeta23/FromPNTPlus/Rectangle.lean x: 2 commits (all time) y: 232 lines of code zeta23/Zeta23/FromPNTPlus/ResidueCalcOnRectangles.lean x: 2 commits (all time) y: 1062 lines of code zeta23/Zeta23/FromPNTPlus/SmoothExistence.lean x: 2 commits (all time) y: 98 lines of code zeta23/Zeta23/FromPNTPlus/StrongPNTPrefix.lean x: 2 commits (all time) y: 459 lines of code zeta23/Zeta23/FromPNTPlus/ZetaBounds.lean x: 2 commits (all time) y: 2788 lines of code zeta23/Zeta23/GammaFacts/IntMu.lean x: 2 commits (all time) y: 515 lines of code zeta23/Zeta23/GammaFacts/Mu.lean x: 2 commits (all time) y: 444 lines of code zeta23/Zeta23/GammaFacts/Series.lean x: 2 commits (all time) y: 478 lines of code zeta23/Zeta23/GammaFacts/StirlingVert.lean x: 2 commits (all time) y: 581 lines of code zeta23/Zeta23/Hypotheses.lean x: 2 commits (all time) y: 140 lines of code zeta23/Zeta23/Hypotheses/GzGp.lean x: 2 commits (all time) y: 130 lines of code zeta23/Zeta23/MV.lean x: 2 commits (all time) y: 212 lines of code zeta23/Zeta23/PairCeiling/LawN256.lean x: 2 commits (all time) y: 287 lines of code zeta23/Zeta23/PiFacts.lean x: 2 commits (all time) y: 408 lines of code zeta23/Zeta23/Poisson.lean x: 2 commits (all time) y: 364 lines of code zeta23/Zeta23/PrimeSideA/Basic.lean x: 2 commits (all time) y: 1276 lines of code zeta23/Zeta23/PrimeSideA/EndsCore.lean x: 2 commits (all time) y: 604 lines of code zeta23/Zeta23/PrimeSideA/EndsE1.lean x: 2 commits (all time) y: 851 lines of code zeta23/Zeta23/PrimeSideA/EndsE2.lean x: 2 commits (all time) y: 431 lines of code zeta23/Zeta23/PrimeSideA/EndsNu.lean x: 2 commits (all time) y: 768 lines of code zeta23/Zeta23/PrimeSideB.lean x: 2 commits (all time) y: 746 lines of code zeta23/Zeta23/PrimeSideB/PPKernel.lean x: 2 commits (all time) y: 642 lines of code zeta23/Zeta23/RvM/Backlund.lean x: 2 commits (all time) y: 383 lines of code zeta23/Zeta23/Taper/Decay.lean x: 2 commits (all time) y: 908 lines of code zeta23/Zeta23/Taper/GevreyRamps.lean x: 2 commits (all time) y: 237 lines of code zeta23/Zeta23/ThmD/Endgame.lean x: 2 commits (all time) y: 414 lines of code zeta23/Zeta23/ThmD/PsiC.lean x: 2 commits (all time) y: 535 lines of code zeta23/Zeta23/ThmD/Window.lean x: 2 commits (all time) y: 1737 lines of code zeta23/Zeta23/ThmE/BacklundChi.lean x: 2 commits (all time) y: 335 lines of code zeta23/Zeta23/ThmE/LGrowth.lean x: 2 commits (all time) y: 317 lines of code zeta23/Zeta23/ThmE/Main.lean x: 2 commits (all time) y: 313 lines of code zeta23/Zeta23/ThmE/MainTermChi.lean x: 2 commits (all time) y: 520 lines of code zeta23/Zeta23/ThmE/PPChi.lean x: 2 commits (all time) y: 946 lines of code zeta23/Zeta23/ThmE/PrimeSideChi.lean x: 2 commits (all time) y: 1381 lines of code zeta23/Zeta23/WeilEF/VerticalLine.lean x: 2 commits (all time) y: 763 lines of code zeta23/Zeta23/XiPrime/ExplicitFormula/Expansion.lean x: 2 commits (all time) y: 1035 lines of code zeta23/Zeta23/XiPrime/ExplicitFormula/TestWeight.lean x: 2 commits (all time) y: 1012 lines of code zeta23/Zeta23/XiPrime/ExplicitFormula/ZeroFree.lean x: 2 commits (all time) y: 1351 lines of code zeta23/Zeta23/XiPrime/Hardy/EFExpansion.lean x: 2 commits (all time) y: 650 lines of code zeta23/Zeta23/XiPrime/QuarticWindow/Moments.lean x: 2 commits (all time) y: 505 lines of code zeta23/Zeta23/XiPrime/Transfer/Dependence.lean x: 2 commits (all time) y: 565 lines of code zeta23/Zeta23/XiPrime/ZeroCount/Generic.lean x: 2 commits (all time) y: 556 lines of code zeta23/Zeta23/ZeroSide.lean x: 2 commits (all time) y: 830 lines of code
3474.0
lines of code
  min: 6.0
  average: 238.52
  25th percentile: 94.0
  median: 170.0
  75th percentile: 306.5
  max: 3474.0
0 5.0
commits (all time)
min: 1.0 | average: 1.45 | 25th percentile: 1.0 | median: 1.0 | 75th percentile: 2.0 | max: 5.0

File Size vs. Contributors (all time): 769 points

3sum-apsp/Challenge/EndStatement.lean x: 1 contributors (all time) y: 71 lines of code 3sum-apsp/Challenge/PaperStatements.lean x: 1 contributors (all time) y: 218 lines of code 3sum-apsp/EndStatement.lean x: 1 contributors (all time) y: 115 lines of code 3sum-apsp/PaperStatements.lean x: 1 contributors (all time) y: 3474 lines of code 3sum-apsp/Solution/EndStatement.lean x: 1 contributors (all time) y: 8 lines of code 3sum-apsp/ThreeSumApsp.lean x: 1 contributors (all time) y: 20 lines of code 3sum-apsp/ThreeSumApsp/ConditionalTimes/Corollary38.lean x: 1 contributors (all time) y: 57 lines of code 3sum-apsp/ThreeSumApsp/ConditionalTimes/Definitions.lean x: 1 contributors (all time) y: 307 lines of code 3sum-apsp/ThreeSumApsp/ConditionalTimes/Theorem34.lean x: 1 contributors (all time) y: 150 lines of code 3sum-apsp/ThreeSumApsp/ConditionalTimes/Theorem35.lean x: 1 contributors (all time) y: 177 lines of code 3sum-apsp/ThreeSumApsp/Lang/Calls.lean x: 1 contributors (all time) y: 104 lines of code 3sum-apsp/ThreeSumApsp/Lang/Compiler/CallFrames.lean x: 1 contributors (all time) y: 134 lines of code 3sum-apsp/ThreeSumApsp/Lang/Compiler/Cells.lean x: 1 contributors (all time) y: 273 lines of code 3sum-apsp/ThreeSumApsp/Lang/Compiler/ProgramCode.lean x: 1 contributors (all time) y: 202 lines of code 3sum-apsp/ThreeSumApsp/Lang/Compiler/Simulation.lean x: 1 contributors (all time) y: 427 lines of code 3sum-apsp/ThreeSumApsp/Lang/Compiler/StatementCode.lean x: 1 contributors (all time) y: 294 lines of code 3sum-apsp/ThreeSumApsp/Lang/Compiler/WholeProgram.lean x: 1 contributors (all time) y: 229 lines of code 3sum-apsp/ThreeSumApsp/Lang/Frames.lean x: 1 contributors (all time) y: 338 lines of code 3sum-apsp/ThreeSumApsp/Lang/Lib/Emod.lean x: 1 contributors (all time) y: 240 lines of code 3sum-apsp/ThreeSumApsp/Lang/Lib/PowTable.lean x: 1 contributors (all time) y: 95 lines of code 3sum-apsp/ThreeSumApsp/Lang/Lib/RadixPass.lean x: 1 contributors (all time) y: 159 lines of code 3sum-apsp/ThreeSumApsp/Lang/Lib/Seg.lean x: 1 contributors (all time) y: 186 lines of code 3sum-apsp/ThreeSumApsp/Lang/Lib/Sieve.lean x: 1 contributors (all time) y: 371 lines of code 3sum-apsp/ThreeSumApsp/Lang/Rules.lean x: 1 contributors (all time) y: 316 lines of code 3sum-apsp/ThreeSumApsp/Lang/ToMachine.lean x: 1 contributors (all time) y: 346 lines of code 3sum-apsp/ThreeSumApsp/Machine/PolylogIsLittleO.lean x: 1 contributors (all time) y: 50 lines of code 3sum-apsp/ThreeSumApsp/Machine/Realized.lean x: 1 contributors (all time) y: 33 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/Contracts.lean x: 1 contributors (all time) y: 502 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/Encode/BandArray.lean x: 1 contributors (all time) y: 669 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/SharedStage.lean x: 1 contributors (all time) y: 601 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/Time.lean x: 1 contributors (all time) y: 286 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/Wanted/Codes.lean x: 1 contributors (all time) y: 633 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Corollary15_16/Split.lean x: 1 contributors (all time) y: 461 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Hashing/Strassen.lean x: 1 contributors (all time) y: 615 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Hashing/ZOrder.lean x: 1 contributors (all time) y: 481 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Host/InstanceFacts.lean x: 1 contributors (all time) y: 402 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Host/Loop.lean x: 1 contributors (all time) y: 580 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Host/Text.lean x: 1 contributors (all time) y: 356 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Instances/WriteMatrices.lean x: 1 contributors (all time) y: 536 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe/Bits.lean x: 1 contributors (all time) y: 412 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe/Contracts.lean x: 1 contributors (all time) y: 440 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe/Modulus.lean x: 1 contributors (all time) y: 565 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe/NodeArray.lean x: 1 contributors (all time) y: 740 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe/Nodes.lean x: 1 contributors (all time) y: 620 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21b/Apsp/Host.lean x: 1 contributors (all time) y: 255 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21b/MinPlus/AllPairs.lean x: 1 contributors (all time) y: 704 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec4/Theorem30/QuerySum.lean x: 1 contributors (all time) y: 390 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec5/Corollary39/MinMaxWeight/Host.lean x: 1 contributors (all time) y: 714 lines of code 3sum-apsp/ThreeSumApsp/RunningTimes/Sec3/Corollary15_16/Layout.lean x: 1 contributors (all time) y: 515 lines of code 3sum-apsp/ThreeSumApsp/Sec2/Lemma10.lean x: 1 contributors (all time) y: 525 lines of code zeta23/Zeta23/LinAlg/HermitianPosPart.lean x: 2 contributors (all time) y: 167 lines of code zeta23/Zeta23/LinAlg/Inertia.lean x: 2 contributors (all time) y: 125 lines of code zeta23/Zeta23/LinAlg/PosIndex.lean x: 2 contributors (all time) y: 103 lines of code zeta23/Zeta23/LinAlg/RankTrace.lean x: 2 contributors (all time) y: 239 lines of code zeta23/Zeta23/LinAlg/Sylvester.lean x: 2 contributors (all time) y: 282 lines of code zeta23/Zeta23/LinAlg/VonNeumann.lean x: 2 contributors (all time) y: 181 lines of code zeta23/Zeta23/LinAlg/Weyl.lean x: 2 contributors (all time) y: 123 lines of code zeta23/formalization.yaml x: 2 contributors (all time) y: 228 lines of code .github/dependabot.yml x: 2 contributors (all time) y: 6 lines of code zeta23/Challenge/XiPrime.lean x: 2 contributors (all time) y: 86 lines of code zeta23/ChallengeDeps/XiPrime.lean x: 2 contributors (all time) y: 32 lines of code zeta23/Solution/XiPrime.lean x: 2 contributors (all time) y: 45 lines of code zeta23/lakefile.toml x: 2 contributors (all time) y: 25 lines of code zeta23/scripts/validate-formalization.rb x: 2 contributors (all time) y: 157 lines of code zeta23/Zeta23/Assembly.lean x: 1 contributors (all time) y: 1451 lines of code zeta23/Zeta23/Chebyshev.lean x: 1 contributors (all time) y: 1144 lines of code zeta23/Zeta23/FromPNTPlus/MediumPNT.lean x: 1 contributors (all time) y: 3387 lines of code zeta23/Zeta23/FromPNTPlus/MellinCalculus.lean x: 1 contributors (all time) y: 974 lines of code zeta23/Zeta23/FromPNTPlus/ResidueCalcOnRectangles.lean x: 1 contributors (all time) y: 1062 lines of code zeta23/Zeta23/FromPNTPlus/ZetaBounds.lean x: 1 contributors (all time) y: 2788 lines of code zeta23/Zeta23/GammaFacts/Series.lean x: 1 contributors (all time) y: 478 lines of code zeta23/Zeta23/PrimeSideA/Basic.lean x: 1 contributors (all time) y: 1276 lines of code zeta23/Zeta23/PrimeSideA/EndsE1.lean x: 1 contributors (all time) y: 851 lines of code zeta23/Zeta23/PrimeSideA/EndsNu.lean x: 1 contributors (all time) y: 768 lines of code zeta23/Zeta23/Taper/Decay.lean x: 1 contributors (all time) y: 908 lines of code zeta23/Zeta23/ThmD/Window.lean x: 1 contributors (all time) y: 1737 lines of code zeta23/Zeta23/ThmE/PPChi.lean x: 1 contributors (all time) y: 946 lines of code zeta23/Zeta23/ThmE/PrimeSideChi.lean x: 1 contributors (all time) y: 1381 lines of code zeta23/Zeta23/WeilEF/VerticalLine.lean x: 1 contributors (all time) y: 763 lines of code zeta23/Zeta23/XiPrime/ExplicitFormula/Expansion.lean x: 1 contributors (all time) y: 1035 lines of code zeta23/Zeta23/XiPrime/ExplicitFormula/TestWeight.lean x: 1 contributors (all time) y: 1012 lines of code zeta23/Zeta23/XiPrime/ExplicitFormula/ZeroFree.lean x: 1 contributors (all time) y: 1351 lines of code zeta23/Zeta23/XiPrime/Hardy/EFExpansion.lean x: 1 contributors (all time) y: 650 lines of code zeta23/Zeta23/XiPrime/ZeroCount/Generic.lean x: 1 contributors (all time) y: 556 lines of code zeta23/Zeta23/ZeroSide.lean x: 1 contributors (all time) y: 830 lines of code
3474.0
lines of code
  min: 6.0
  average: 238.52
  25th percentile: 94.0
  median: 170.0
  75th percentile: 306.5
  max: 3474.0
0 2.0
contributors (all time)
min: 1.0 | average: 1.03 | 25th percentile: 1.0 | median: 1.0 | 75th percentile: 1.0 | max: 2.0

File Size vs. Commits (30 days): 438 points

3sum-apsp/Challenge/EndStatement.lean x: 1 commits (30d) y: 71 lines of code 3sum-apsp/Challenge/PaperStatements.lean x: 1 commits (30d) y: 218 lines of code 3sum-apsp/EndStatement.lean x: 1 commits (30d) y: 115 lines of code 3sum-apsp/PaperStatements.lean x: 1 commits (30d) y: 3474 lines of code 3sum-apsp/Solution/EndStatement.lean x: 1 commits (30d) y: 8 lines of code 3sum-apsp/ThreeSumApsp.lean x: 1 commits (30d) y: 20 lines of code 3sum-apsp/ThreeSumApsp/ConditionalTimes/Corollary38.lean x: 1 commits (30d) y: 57 lines of code 3sum-apsp/ThreeSumApsp/ConditionalTimes/Definitions.lean x: 1 commits (30d) y: 307 lines of code 3sum-apsp/ThreeSumApsp/ConditionalTimes/Theorem34.lean x: 1 commits (30d) y: 150 lines of code 3sum-apsp/ThreeSumApsp/ConditionalTimes/Theorem35.lean x: 1 commits (30d) y: 177 lines of code 3sum-apsp/ThreeSumApsp/Lang/Calls.lean x: 1 commits (30d) y: 104 lines of code 3sum-apsp/ThreeSumApsp/Lang/Compiler/CallFrames.lean x: 1 commits (30d) y: 134 lines of code 3sum-apsp/ThreeSumApsp/Lang/Compiler/Cells.lean x: 1 commits (30d) y: 273 lines of code 3sum-apsp/ThreeSumApsp/Lang/Compiler/ProgramCode.lean x: 1 commits (30d) y: 202 lines of code 3sum-apsp/ThreeSumApsp/Lang/Compiler/Simulation.lean x: 1 commits (30d) y: 427 lines of code 3sum-apsp/ThreeSumApsp/Lang/Compiler/StatementCode.lean x: 1 commits (30d) y: 294 lines of code 3sum-apsp/ThreeSumApsp/Lang/Compiler/WholeProgram.lean x: 1 commits (30d) y: 229 lines of code 3sum-apsp/ThreeSumApsp/Lang/Frames.lean x: 1 commits (30d) y: 338 lines of code 3sum-apsp/ThreeSumApsp/Lang/Lib/Emod.lean x: 1 commits (30d) y: 240 lines of code 3sum-apsp/ThreeSumApsp/Lang/Lib/PowTable.lean x: 1 commits (30d) y: 95 lines of code 3sum-apsp/ThreeSumApsp/Lang/Lib/RadixPass.lean x: 1 commits (30d) y: 159 lines of code 3sum-apsp/ThreeSumApsp/Lang/Lib/Seg.lean x: 1 commits (30d) y: 186 lines of code 3sum-apsp/ThreeSumApsp/Lang/Lib/Sieve.lean x: 1 commits (30d) y: 371 lines of code 3sum-apsp/ThreeSumApsp/Lang/Rules.lean x: 1 commits (30d) y: 316 lines of code 3sum-apsp/ThreeSumApsp/Lang/ToMachine.lean x: 1 commits (30d) y: 346 lines of code 3sum-apsp/ThreeSumApsp/Machine/PolylogIsLittleO.lean x: 1 commits (30d) y: 50 lines of code 3sum-apsp/ThreeSumApsp/Machine/Realized.lean x: 1 commits (30d) y: 33 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/Contracts.lean x: 1 commits (30d) y: 502 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/Encode/BandArray.lean x: 1 commits (30d) y: 669 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/SharedStage.lean x: 1 commits (30d) y: 601 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/Time.lean x: 1 commits (30d) y: 286 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/Wanted/Codes.lean x: 1 commits (30d) y: 633 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Corollary15_16/Split.lean x: 1 commits (30d) y: 461 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Hashing/Strassen.lean x: 1 commits (30d) y: 615 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Hashing/ZOrder.lean x: 1 commits (30d) y: 481 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Host/InstanceFacts.lean x: 1 commits (30d) y: 402 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Host/Loop.lean x: 1 commits (30d) y: 580 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Host/Text.lean x: 1 commits (30d) y: 356 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Instances/WriteMatrices.lean x: 1 commits (30d) y: 536 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe/Bits.lean x: 1 commits (30d) y: 412 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe/Contracts.lean x: 1 commits (30d) y: 440 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe/Modulus.lean x: 1 commits (30d) y: 565 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe/NodeArray.lean x: 1 commits (30d) y: 740 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe/Nodes.lean x: 1 commits (30d) y: 620 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21b/Apsp/Host.lean x: 1 commits (30d) y: 255 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21b/MinPlus/AllPairs.lean x: 1 commits (30d) y: 704 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec4/Theorem30/QuerySum.lean x: 1 commits (30d) y: 390 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec5/Corollary39/MinMaxWeight/Host.lean x: 1 commits (30d) y: 714 lines of code 3sum-apsp/ThreeSumApsp/RunningTimes/Sec3/Corollary15_16/Layout.lean x: 1 commits (30d) y: 515 lines of code 3sum-apsp/ThreeSumApsp/Sec2/Lemma10.lean x: 1 commits (30d) y: 525 lines of code
3474.0
lines of code
  min: 8.0
  average: 203.16
  25th percentile: 91.0
  median: 150.5
  75th percentile: 271.25
  max: 3474.0
0 1.0
commits (30d)
min: 1.0 | average: 1.0 | 25th percentile: 1.0 | median: 1.0 | 75th percentile: 1.0 | max: 1.0

File Size vs. Contributors (30 days): 438 points

3sum-apsp/Challenge/EndStatement.lean x: 1 contributors (30d) y: 71 lines of code 3sum-apsp/Challenge/PaperStatements.lean x: 1 contributors (30d) y: 218 lines of code 3sum-apsp/EndStatement.lean x: 1 contributors (30d) y: 115 lines of code 3sum-apsp/PaperStatements.lean x: 1 contributors (30d) y: 3474 lines of code 3sum-apsp/Solution/EndStatement.lean x: 1 contributors (30d) y: 8 lines of code 3sum-apsp/ThreeSumApsp.lean x: 1 contributors (30d) y: 20 lines of code 3sum-apsp/ThreeSumApsp/ConditionalTimes/Corollary38.lean x: 1 contributors (30d) y: 57 lines of code 3sum-apsp/ThreeSumApsp/ConditionalTimes/Definitions.lean x: 1 contributors (30d) y: 307 lines of code 3sum-apsp/ThreeSumApsp/ConditionalTimes/Theorem34.lean x: 1 contributors (30d) y: 150 lines of code 3sum-apsp/ThreeSumApsp/ConditionalTimes/Theorem35.lean x: 1 contributors (30d) y: 177 lines of code 3sum-apsp/ThreeSumApsp/Lang/Calls.lean x: 1 contributors (30d) y: 104 lines of code 3sum-apsp/ThreeSumApsp/Lang/Compiler/CallFrames.lean x: 1 contributors (30d) y: 134 lines of code 3sum-apsp/ThreeSumApsp/Lang/Compiler/Cells.lean x: 1 contributors (30d) y: 273 lines of code 3sum-apsp/ThreeSumApsp/Lang/Compiler/ProgramCode.lean x: 1 contributors (30d) y: 202 lines of code 3sum-apsp/ThreeSumApsp/Lang/Compiler/Simulation.lean x: 1 contributors (30d) y: 427 lines of code 3sum-apsp/ThreeSumApsp/Lang/Compiler/StatementCode.lean x: 1 contributors (30d) y: 294 lines of code 3sum-apsp/ThreeSumApsp/Lang/Compiler/WholeProgram.lean x: 1 contributors (30d) y: 229 lines of code 3sum-apsp/ThreeSumApsp/Lang/Frames.lean x: 1 contributors (30d) y: 338 lines of code 3sum-apsp/ThreeSumApsp/Lang/Lib/Emod.lean x: 1 contributors (30d) y: 240 lines of code 3sum-apsp/ThreeSumApsp/Lang/Lib/PowTable.lean x: 1 contributors (30d) y: 95 lines of code 3sum-apsp/ThreeSumApsp/Lang/Lib/RadixPass.lean x: 1 contributors (30d) y: 159 lines of code 3sum-apsp/ThreeSumApsp/Lang/Lib/Seg.lean x: 1 contributors (30d) y: 186 lines of code 3sum-apsp/ThreeSumApsp/Lang/Lib/Sieve.lean x: 1 contributors (30d) y: 371 lines of code 3sum-apsp/ThreeSumApsp/Lang/Rules.lean x: 1 contributors (30d) y: 316 lines of code 3sum-apsp/ThreeSumApsp/Lang/ToMachine.lean x: 1 contributors (30d) y: 346 lines of code 3sum-apsp/ThreeSumApsp/Machine/PolylogIsLittleO.lean x: 1 contributors (30d) y: 50 lines of code 3sum-apsp/ThreeSumApsp/Machine/Realized.lean x: 1 contributors (30d) y: 33 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/Contracts.lean x: 1 contributors (30d) y: 502 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/Encode/BandArray.lean x: 1 contributors (30d) y: 669 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/SharedStage.lean x: 1 contributors (30d) y: 601 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/Time.lean x: 1 contributors (30d) y: 286 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/Wanted/Codes.lean x: 1 contributors (30d) y: 633 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Corollary15_16/Split.lean x: 1 contributors (30d) y: 461 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Hashing/Strassen.lean x: 1 contributors (30d) y: 615 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Hashing/ZOrder.lean x: 1 contributors (30d) y: 481 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Host/InstanceFacts.lean x: 1 contributors (30d) y: 402 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Host/Loop.lean x: 1 contributors (30d) y: 580 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Host/Text.lean x: 1 contributors (30d) y: 356 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Instances/WriteMatrices.lean x: 1 contributors (30d) y: 536 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe/Bits.lean x: 1 contributors (30d) y: 412 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe/Contracts.lean x: 1 contributors (30d) y: 440 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe/Modulus.lean x: 1 contributors (30d) y: 565 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe/NodeArray.lean x: 1 contributors (30d) y: 740 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe/Nodes.lean x: 1 contributors (30d) y: 620 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21b/Apsp/Host.lean x: 1 contributors (30d) y: 255 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21b/MinPlus/AllPairs.lean x: 1 contributors (30d) y: 704 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec4/Theorem30/QuerySum.lean x: 1 contributors (30d) y: 390 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec5/Corollary39/MinMaxWeight/Host.lean x: 1 contributors (30d) y: 714 lines of code 3sum-apsp/ThreeSumApsp/RunningTimes/Sec3/Corollary15_16/Layout.lean x: 1 contributors (30d) y: 515 lines of code 3sum-apsp/ThreeSumApsp/Sec2/Lemma10.lean x: 1 contributors (30d) y: 525 lines of code
3474.0
lines of code
  min: 8.0
  average: 203.16
  25th percentile: 91.0
  median: 150.5
  75th percentile: 271.25
  max: 3474.0
0 1.0
contributors (30d)
min: 1.0 | average: 1.0 | 25th percentile: 1.0 | median: 1.0 | 75th percentile: 1.0 | max: 1.0

File Size vs. Commits (90 days): 769 points

3sum-apsp/Challenge/EndStatement.lean x: 1 commits (90d) y: 71 lines of code 3sum-apsp/Challenge/PaperStatements.lean x: 1 commits (90d) y: 218 lines of code 3sum-apsp/EndStatement.lean x: 1 commits (90d) y: 115 lines of code 3sum-apsp/PaperStatements.lean x: 1 commits (90d) y: 3474 lines of code 3sum-apsp/Solution/EndStatement.lean x: 1 commits (90d) y: 8 lines of code 3sum-apsp/ThreeSumApsp.lean x: 1 commits (90d) y: 20 lines of code 3sum-apsp/ThreeSumApsp/ConditionalTimes/Corollary38.lean x: 1 commits (90d) y: 57 lines of code 3sum-apsp/ThreeSumApsp/ConditionalTimes/Definitions.lean x: 1 commits (90d) y: 307 lines of code 3sum-apsp/ThreeSumApsp/ConditionalTimes/Theorem34.lean x: 1 commits (90d) y: 150 lines of code 3sum-apsp/ThreeSumApsp/ConditionalTimes/Theorem35.lean x: 1 commits (90d) y: 177 lines of code 3sum-apsp/ThreeSumApsp/Lang/Calls.lean x: 1 commits (90d) y: 104 lines of code 3sum-apsp/ThreeSumApsp/Lang/Compiler/CallFrames.lean x: 1 commits (90d) y: 134 lines of code 3sum-apsp/ThreeSumApsp/Lang/Compiler/Cells.lean x: 1 commits (90d) y: 273 lines of code 3sum-apsp/ThreeSumApsp/Lang/Compiler/ProgramCode.lean x: 1 commits (90d) y: 202 lines of code 3sum-apsp/ThreeSumApsp/Lang/Compiler/Simulation.lean x: 1 commits (90d) y: 427 lines of code 3sum-apsp/ThreeSumApsp/Lang/Compiler/StatementCode.lean x: 1 commits (90d) y: 294 lines of code 3sum-apsp/ThreeSumApsp/Lang/Compiler/WholeProgram.lean x: 1 commits (90d) y: 229 lines of code 3sum-apsp/ThreeSumApsp/Lang/Frames.lean x: 1 commits (90d) y: 338 lines of code 3sum-apsp/ThreeSumApsp/Lang/Lib/Emod.lean x: 1 commits (90d) y: 240 lines of code 3sum-apsp/ThreeSumApsp/Lang/Lib/PowTable.lean x: 1 commits (90d) y: 95 lines of code 3sum-apsp/ThreeSumApsp/Lang/Lib/RadixPass.lean x: 1 commits (90d) y: 159 lines of code 3sum-apsp/ThreeSumApsp/Lang/Lib/Seg.lean x: 1 commits (90d) y: 186 lines of code 3sum-apsp/ThreeSumApsp/Lang/Lib/Sieve.lean x: 1 commits (90d) y: 371 lines of code 3sum-apsp/ThreeSumApsp/Lang/Rules.lean x: 1 commits (90d) y: 316 lines of code 3sum-apsp/ThreeSumApsp/Lang/ToMachine.lean x: 1 commits (90d) y: 346 lines of code 3sum-apsp/ThreeSumApsp/Machine/PolylogIsLittleO.lean x: 1 commits (90d) y: 50 lines of code 3sum-apsp/ThreeSumApsp/Machine/Realized.lean x: 1 commits (90d) y: 33 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/Contracts.lean x: 1 commits (90d) y: 502 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/Encode/BandArray.lean x: 1 commits (90d) y: 669 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/SharedStage.lean x: 1 commits (90d) y: 601 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/Time.lean x: 1 commits (90d) y: 286 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/Wanted/Codes.lean x: 1 commits (90d) y: 633 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Corollary15_16/Split.lean x: 1 commits (90d) y: 461 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Hashing/Strassen.lean x: 1 commits (90d) y: 615 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Hashing/ZOrder.lean x: 1 commits (90d) y: 481 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Host/InstanceFacts.lean x: 1 commits (90d) y: 402 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Host/Loop.lean x: 1 commits (90d) y: 580 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Host/Text.lean x: 1 commits (90d) y: 356 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Instances/WriteMatrices.lean x: 1 commits (90d) y: 536 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe/Bits.lean x: 1 commits (90d) y: 412 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe/Contracts.lean x: 1 commits (90d) y: 440 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe/Modulus.lean x: 1 commits (90d) y: 565 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe/NodeArray.lean x: 1 commits (90d) y: 740 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe/Nodes.lean x: 1 commits (90d) y: 620 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21b/Apsp/Host.lean x: 1 commits (90d) y: 255 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21b/MinPlus/AllPairs.lean x: 1 commits (90d) y: 704 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec4/Theorem30/QuerySum.lean x: 1 commits (90d) y: 390 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec5/Corollary39/MinMaxWeight/Host.lean x: 1 commits (90d) y: 714 lines of code 3sum-apsp/ThreeSumApsp/RunningTimes/Sec3/Corollary15_16/Layout.lean x: 1 commits (90d) y: 515 lines of code 3sum-apsp/ThreeSumApsp/Sec2/Lemma10.lean x: 1 commits (90d) y: 525 lines of code zeta23/Zeta23/LinAlg/HermitianPosPart.lean x: 3 commits (90d) y: 167 lines of code zeta23/Zeta23/LinAlg/Inertia.lean x: 3 commits (90d) y: 125 lines of code zeta23/Zeta23/LinAlg/PosIndex.lean x: 3 commits (90d) y: 103 lines of code zeta23/Zeta23/LinAlg/RankTrace.lean x: 3 commits (90d) y: 239 lines of code zeta23/Zeta23/LinAlg/Sylvester.lean x: 3 commits (90d) y: 282 lines of code zeta23/Zeta23/LinAlg/VonNeumann.lean x: 3 commits (90d) y: 181 lines of code zeta23/Zeta23/LinAlg/Weyl.lean x: 3 commits (90d) y: 123 lines of code zeta23/formalization.yaml x: 5 commits (90d) y: 228 lines of code .github/dependabot.yml x: 2 commits (90d) y: 6 lines of code zeta23/Challenge.lean x: 2 commits (90d) y: 188 lines of code zeta23/Challenge/XiPrime.lean x: 2 commits (90d) y: 86 lines of code zeta23/ChallengeDeps/XiPrime.lean x: 2 commits (90d) y: 32 lines of code zeta23/Solution.lean x: 2 commits (90d) y: 119 lines of code zeta23/Solution/XiPrime.lean x: 2 commits (90d) y: 45 lines of code zeta23/lakefile.toml x: 4 commits (90d) y: 25 lines of code zeta23/scripts/PrintAxioms/PairCeiling.lean x: 2 commits (90d) y: 20 lines of code zeta23/scripts/validate-formalization.rb x: 2 commits (90d) y: 157 lines of code zeta23/Zeta23/Analytic/RectangleLogDeriv.lean x: 2 commits (90d) y: 373 lines of code zeta23/Zeta23/Analytic/Stirling.lean x: 2 commits (90d) y: 272 lines of code zeta23/Zeta23/Assembly.lean x: 2 commits (90d) y: 1451 lines of code zeta23/Zeta23/Assembly/Inputs.lean x: 2 commits (90d) y: 59 lines of code zeta23/Zeta23/Chebyshev.lean x: 2 commits (90d) y: 1144 lines of code zeta23/Zeta23/Defs.lean x: 2 commits (90d) y: 252 lines of code zeta23/Zeta23/Defs/LeafIntegrals.lean x: 2 commits (90d) y: 196 lines of code zeta23/Zeta23/ExplicitFormula.lean x: 2 commits (90d) y: 662 lines of code zeta23/Zeta23/Final.lean x: 2 commits (90d) y: 299 lines of code zeta23/Zeta23/FinalMult.lean x: 2 commits (90d) y: 345 lines of code zeta23/Zeta23/FromPNTPlus/Auxiliary.lean x: 2 commits (90d) y: 73 lines of code zeta23/Zeta23/FromPNTPlus/MediumPNT.lean x: 2 commits (90d) y: 3387 lines of code zeta23/Zeta23/FromPNTPlus/MellinCalculus.lean x: 2 commits (90d) y: 974 lines of code zeta23/Zeta23/FromPNTPlus/Mertens.lean x: 2 commits (90d) y: 177 lines of code zeta23/Zeta23/FromPNTPlus/Rectangle.lean x: 2 commits (90d) y: 232 lines of code zeta23/Zeta23/FromPNTPlus/ResidueCalcOnRectangles.lean x: 2 commits (90d) y: 1062 lines of code zeta23/Zeta23/FromPNTPlus/SmoothExistence.lean x: 2 commits (90d) y: 98 lines of code zeta23/Zeta23/FromPNTPlus/StrongPNTPrefix.lean x: 2 commits (90d) y: 459 lines of code zeta23/Zeta23/FromPNTPlus/ZetaBounds.lean x: 2 commits (90d) y: 2788 lines of code zeta23/Zeta23/GammaFacts/IntMu.lean x: 2 commits (90d) y: 515 lines of code zeta23/Zeta23/GammaFacts/Mu.lean x: 2 commits (90d) y: 444 lines of code zeta23/Zeta23/GammaFacts/Series.lean x: 2 commits (90d) y: 478 lines of code zeta23/Zeta23/GammaFacts/StirlingVert.lean x: 2 commits (90d) y: 581 lines of code zeta23/Zeta23/Hypotheses.lean x: 2 commits (90d) y: 140 lines of code zeta23/Zeta23/Hypotheses/GzGp.lean x: 2 commits (90d) y: 130 lines of code zeta23/Zeta23/MV.lean x: 2 commits (90d) y: 212 lines of code zeta23/Zeta23/PairCeiling/LawN256.lean x: 2 commits (90d) y: 287 lines of code zeta23/Zeta23/PiFacts.lean x: 2 commits (90d) y: 408 lines of code zeta23/Zeta23/Poisson.lean x: 2 commits (90d) y: 364 lines of code zeta23/Zeta23/PrimeSideA/Basic.lean x: 2 commits (90d) y: 1276 lines of code zeta23/Zeta23/PrimeSideA/EndsCore.lean x: 2 commits (90d) y: 604 lines of code zeta23/Zeta23/PrimeSideA/EndsE1.lean x: 2 commits (90d) y: 851 lines of code zeta23/Zeta23/PrimeSideA/EndsE2.lean x: 2 commits (90d) y: 431 lines of code zeta23/Zeta23/PrimeSideA/EndsNu.lean x: 2 commits (90d) y: 768 lines of code zeta23/Zeta23/PrimeSideB.lean x: 2 commits (90d) y: 746 lines of code zeta23/Zeta23/PrimeSideB/PPKernel.lean x: 2 commits (90d) y: 642 lines of code zeta23/Zeta23/RvM/Backlund.lean x: 2 commits (90d) y: 383 lines of code zeta23/Zeta23/Taper/Decay.lean x: 2 commits (90d) y: 908 lines of code zeta23/Zeta23/Taper/GevreyRamps.lean x: 2 commits (90d) y: 237 lines of code zeta23/Zeta23/ThmD/Endgame.lean x: 2 commits (90d) y: 414 lines of code zeta23/Zeta23/ThmD/PsiC.lean x: 2 commits (90d) y: 535 lines of code zeta23/Zeta23/ThmD/Window.lean x: 2 commits (90d) y: 1737 lines of code zeta23/Zeta23/ThmE/BacklundChi.lean x: 2 commits (90d) y: 335 lines of code zeta23/Zeta23/ThmE/LGrowth.lean x: 2 commits (90d) y: 317 lines of code zeta23/Zeta23/ThmE/Main.lean x: 2 commits (90d) y: 313 lines of code zeta23/Zeta23/ThmE/MainTermChi.lean x: 2 commits (90d) y: 520 lines of code zeta23/Zeta23/ThmE/PPChi.lean x: 2 commits (90d) y: 946 lines of code zeta23/Zeta23/ThmE/PrimeSideChi.lean x: 2 commits (90d) y: 1381 lines of code zeta23/Zeta23/WeilEF/VerticalLine.lean x: 2 commits (90d) y: 763 lines of code zeta23/Zeta23/XiPrime/ExplicitFormula/Expansion.lean x: 2 commits (90d) y: 1035 lines of code zeta23/Zeta23/XiPrime/ExplicitFormula/TestWeight.lean x: 2 commits (90d) y: 1012 lines of code zeta23/Zeta23/XiPrime/ExplicitFormula/ZeroFree.lean x: 2 commits (90d) y: 1351 lines of code zeta23/Zeta23/XiPrime/Hardy/EFExpansion.lean x: 2 commits (90d) y: 650 lines of code zeta23/Zeta23/XiPrime/QuarticWindow/Moments.lean x: 2 commits (90d) y: 505 lines of code zeta23/Zeta23/XiPrime/Transfer/Dependence.lean x: 2 commits (90d) y: 565 lines of code zeta23/Zeta23/XiPrime/ZeroCount/Generic.lean x: 2 commits (90d) y: 556 lines of code zeta23/Zeta23/ZeroSide.lean x: 2 commits (90d) y: 830 lines of code
3474.0
lines of code
  min: 6.0
  average: 238.52
  25th percentile: 94.0
  median: 170.0
  75th percentile: 306.5
  max: 3474.0
0 5.0
commits (90d)
min: 1.0 | average: 1.45 | 25th percentile: 1.0 | median: 1.0 | 75th percentile: 2.0 | max: 5.0

File Size vs. Contributors (90 days): 769 points

3sum-apsp/Challenge/EndStatement.lean x: 1 contributors (90d) y: 71 lines of code 3sum-apsp/Challenge/PaperStatements.lean x: 1 contributors (90d) y: 218 lines of code 3sum-apsp/EndStatement.lean x: 1 contributors (90d) y: 115 lines of code 3sum-apsp/PaperStatements.lean x: 1 contributors (90d) y: 3474 lines of code 3sum-apsp/Solution/EndStatement.lean x: 1 contributors (90d) y: 8 lines of code 3sum-apsp/ThreeSumApsp.lean x: 1 contributors (90d) y: 20 lines of code 3sum-apsp/ThreeSumApsp/ConditionalTimes/Corollary38.lean x: 1 contributors (90d) y: 57 lines of code 3sum-apsp/ThreeSumApsp/ConditionalTimes/Definitions.lean x: 1 contributors (90d) y: 307 lines of code 3sum-apsp/ThreeSumApsp/ConditionalTimes/Theorem34.lean x: 1 contributors (90d) y: 150 lines of code 3sum-apsp/ThreeSumApsp/ConditionalTimes/Theorem35.lean x: 1 contributors (90d) y: 177 lines of code 3sum-apsp/ThreeSumApsp/Lang/Calls.lean x: 1 contributors (90d) y: 104 lines of code 3sum-apsp/ThreeSumApsp/Lang/Compiler/CallFrames.lean x: 1 contributors (90d) y: 134 lines of code 3sum-apsp/ThreeSumApsp/Lang/Compiler/Cells.lean x: 1 contributors (90d) y: 273 lines of code 3sum-apsp/ThreeSumApsp/Lang/Compiler/ProgramCode.lean x: 1 contributors (90d) y: 202 lines of code 3sum-apsp/ThreeSumApsp/Lang/Compiler/Simulation.lean x: 1 contributors (90d) y: 427 lines of code 3sum-apsp/ThreeSumApsp/Lang/Compiler/StatementCode.lean x: 1 contributors (90d) y: 294 lines of code 3sum-apsp/ThreeSumApsp/Lang/Compiler/WholeProgram.lean x: 1 contributors (90d) y: 229 lines of code 3sum-apsp/ThreeSumApsp/Lang/Frames.lean x: 1 contributors (90d) y: 338 lines of code 3sum-apsp/ThreeSumApsp/Lang/Lib/Emod.lean x: 1 contributors (90d) y: 240 lines of code 3sum-apsp/ThreeSumApsp/Lang/Lib/PowTable.lean x: 1 contributors (90d) y: 95 lines of code 3sum-apsp/ThreeSumApsp/Lang/Lib/RadixPass.lean x: 1 contributors (90d) y: 159 lines of code 3sum-apsp/ThreeSumApsp/Lang/Lib/Seg.lean x: 1 contributors (90d) y: 186 lines of code 3sum-apsp/ThreeSumApsp/Lang/Lib/Sieve.lean x: 1 contributors (90d) y: 371 lines of code 3sum-apsp/ThreeSumApsp/Lang/Rules.lean x: 1 contributors (90d) y: 316 lines of code 3sum-apsp/ThreeSumApsp/Lang/ToMachine.lean x: 1 contributors (90d) y: 346 lines of code 3sum-apsp/ThreeSumApsp/Machine/PolylogIsLittleO.lean x: 1 contributors (90d) y: 50 lines of code 3sum-apsp/ThreeSumApsp/Machine/Realized.lean x: 1 contributors (90d) y: 33 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/Contracts.lean x: 1 contributors (90d) y: 502 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/Encode/BandArray.lean x: 1 contributors (90d) y: 669 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/SharedStage.lean x: 1 contributors (90d) y: 601 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/Time.lean x: 1 contributors (90d) y: 286 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/Wanted/Codes.lean x: 1 contributors (90d) y: 633 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Corollary15_16/Split.lean x: 1 contributors (90d) y: 461 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Hashing/Strassen.lean x: 1 contributors (90d) y: 615 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Hashing/ZOrder.lean x: 1 contributors (90d) y: 481 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Host/InstanceFacts.lean x: 1 contributors (90d) y: 402 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Host/Loop.lean x: 1 contributors (90d) y: 580 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Host/Text.lean x: 1 contributors (90d) y: 356 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Instances/WriteMatrices.lean x: 1 contributors (90d) y: 536 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe/Bits.lean x: 1 contributors (90d) y: 412 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe/Contracts.lean x: 1 contributors (90d) y: 440 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe/Modulus.lean x: 1 contributors (90d) y: 565 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe/NodeArray.lean x: 1 contributors (90d) y: 740 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe/Nodes.lean x: 1 contributors (90d) y: 620 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21b/Apsp/Host.lean x: 1 contributors (90d) y: 255 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21b/MinPlus/AllPairs.lean x: 1 contributors (90d) y: 704 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec4/Theorem30/QuerySum.lean x: 1 contributors (90d) y: 390 lines of code 3sum-apsp/ThreeSumApsp/Programs/Sec5/Corollary39/MinMaxWeight/Host.lean x: 1 contributors (90d) y: 714 lines of code 3sum-apsp/ThreeSumApsp/RunningTimes/Sec3/Corollary15_16/Layout.lean x: 1 contributors (90d) y: 515 lines of code 3sum-apsp/ThreeSumApsp/Sec2/Lemma10.lean x: 1 contributors (90d) y: 525 lines of code zeta23/Zeta23/LinAlg/HermitianPosPart.lean x: 2 contributors (90d) y: 167 lines of code zeta23/Zeta23/LinAlg/Inertia.lean x: 2 contributors (90d) y: 125 lines of code zeta23/Zeta23/LinAlg/PosIndex.lean x: 2 contributors (90d) y: 103 lines of code zeta23/Zeta23/LinAlg/RankTrace.lean x: 2 contributors (90d) y: 239 lines of code zeta23/Zeta23/LinAlg/Sylvester.lean x: 2 contributors (90d) y: 282 lines of code zeta23/Zeta23/LinAlg/VonNeumann.lean x: 2 contributors (90d) y: 181 lines of code zeta23/Zeta23/LinAlg/Weyl.lean x: 2 contributors (90d) y: 123 lines of code zeta23/formalization.yaml x: 2 contributors (90d) y: 228 lines of code .github/dependabot.yml x: 2 contributors (90d) y: 6 lines of code zeta23/Challenge/XiPrime.lean x: 2 contributors (90d) y: 86 lines of code zeta23/ChallengeDeps/XiPrime.lean x: 2 contributors (90d) y: 32 lines of code zeta23/Solution/XiPrime.lean x: 2 contributors (90d) y: 45 lines of code zeta23/lakefile.toml x: 2 contributors (90d) y: 25 lines of code zeta23/scripts/validate-formalization.rb x: 2 contributors (90d) y: 157 lines of code zeta23/Zeta23/Assembly.lean x: 1 contributors (90d) y: 1451 lines of code zeta23/Zeta23/Chebyshev.lean x: 1 contributors (90d) y: 1144 lines of code zeta23/Zeta23/FromPNTPlus/MediumPNT.lean x: 1 contributors (90d) y: 3387 lines of code zeta23/Zeta23/FromPNTPlus/MellinCalculus.lean x: 1 contributors (90d) y: 974 lines of code zeta23/Zeta23/FromPNTPlus/ResidueCalcOnRectangles.lean x: 1 contributors (90d) y: 1062 lines of code zeta23/Zeta23/FromPNTPlus/ZetaBounds.lean x: 1 contributors (90d) y: 2788 lines of code zeta23/Zeta23/GammaFacts/Series.lean x: 1 contributors (90d) y: 478 lines of code zeta23/Zeta23/PrimeSideA/Basic.lean x: 1 contributors (90d) y: 1276 lines of code zeta23/Zeta23/PrimeSideA/EndsE1.lean x: 1 contributors (90d) y: 851 lines of code zeta23/Zeta23/PrimeSideA/EndsNu.lean x: 1 contributors (90d) y: 768 lines of code zeta23/Zeta23/Taper/Decay.lean x: 1 contributors (90d) y: 908 lines of code zeta23/Zeta23/ThmD/Window.lean x: 1 contributors (90d) y: 1737 lines of code zeta23/Zeta23/ThmE/PPChi.lean x: 1 contributors (90d) y: 946 lines of code zeta23/Zeta23/ThmE/PrimeSideChi.lean x: 1 contributors (90d) y: 1381 lines of code zeta23/Zeta23/WeilEF/VerticalLine.lean x: 1 contributors (90d) y: 763 lines of code zeta23/Zeta23/XiPrime/ExplicitFormula/Expansion.lean x: 1 contributors (90d) y: 1035 lines of code zeta23/Zeta23/XiPrime/ExplicitFormula/TestWeight.lean x: 1 contributors (90d) y: 1012 lines of code zeta23/Zeta23/XiPrime/ExplicitFormula/ZeroFree.lean x: 1 contributors (90d) y: 1351 lines of code zeta23/Zeta23/XiPrime/Hardy/EFExpansion.lean x: 1 contributors (90d) y: 650 lines of code zeta23/Zeta23/XiPrime/ZeroCount/Generic.lean x: 1 contributors (90d) y: 556 lines of code zeta23/Zeta23/ZeroSide.lean x: 1 contributors (90d) y: 830 lines of code
3474.0
lines of code
  min: 6.0
  average: 238.52
  25th percentile: 94.0
  median: 170.0
  75th percentile: 306.5
  max: 3474.0
0 2.0
contributors (90d)
min: 1.0 | average: 1.03 | 25th percentile: 1.0 | median: 1.0 | 75th percentile: 1.0 | max: 2.0
About This Analysis
  • File size measurements show the distribution of size of files.
  • Files are classified in four categories based on their size (lines of code): 1-100 (very small files), 101-200 (small files), 201-500 (medium size files), 501-1000 (long files), 1001+(very long files).
  • It is a good practice to keep files small. Long files may become "bloaters", code that have increased to such gargantuan proportions that they are hard to work with.
Learn more...