File Size Overall
  • There are 129,381 files with 22,372,333 lines of code.
    • 2,132 very long files (4,461,559 lines of code)
    • 6,350 long files (4,292,500 lines of code)
    • 15,545 medium size files (4,898,232 lines of code)
    • 29,969 small files (4,110,289 lines of code)
    • 75,385 very small files (4,609,753 lines of code)
19% | 19% | 21% | 18% | 20%
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
lean20% | 17% | 20% | 19% | 22%
tex18% | 36% | 31% | 8% | 4%
yaml100% | 0% | 0% | 0% | 0%
bib<1% | 15% | 61% | 20% | 1%
cpp0% | 30% | 21% | 33% | 13%
py0% | 3% | 45% | 32% | 18%
hpp0% | 0% | 100% | 0% | 0%
jsonl0% | 0% | 0% | 100% | 0%
File Size per Logical Decomposition
primary
1001+
501-1000
201-500
101-200
1-100
lean20% | 17% | 20% | 19% | 22%
preprints17% | 35% | 33% | 9% | 4%
reasoning_traces0% | 0% | 0% | 100% | 0%
Longest Files (Top 50)
File# lines# units
lean
GeodesicGeometry05.lean
in lean/OAI/Geometry/EinsteinFour
8586 -
lean
FormalBoxes.lean
in lean/OAI/Geometry/SplitTangent
8136 -
tex
paper.tex
in preprints/Weil-classes-and-Hodge-classes-on-abelian-powers-September-30-2026/build
7720 -
lean
CoverageK12.lean
in lean/OAI/Combinatorics/Ramsey/CycleClique/Construction
7607 -
lean
IndexedFillingValue.lean
in lean/OAI/Geometry/HyperbolicGroups
6961 -
lean
LocalScarcity.lean
in lean/OAI/Dynamics/StandardMap
6886 -
lean
TailEnergy.lean
in lean/OAI/Geometry/Relativity/CKS
6418 -
lean
Sources81.lean
in lean/OAI/Analysis/MutuallyUnbiased/MixedSemantics
6205 -
lean
Sources33.lean
in lean/OAI/Analysis/MutuallyUnbiased/MixedSemantics
6176 -
lean
Sources82.lean
in lean/OAI/Analysis/MutuallyUnbiased/MixedSemantics
6069 -
lean
Sources34.lean
in lean/OAI/Analysis/MutuallyUnbiased/MixedSemantics
6045 -
lean
Sources0.lean
in lean/OAI/Analysis/MutuallyUnbiased/MixedSemantics
5884 -
lean
Sources26.lean
in lean/OAI/Analysis/MutuallyUnbiased/MixedSemantics
5756 -
lean
CoarseAssembly.lean
in lean/ComparatorChallenges
5687 -
lean
Definitions.lean
in lean/OAI/Topology/CoarseAssembly
5674 -
lean
Sources80.lean
in lean/OAI/Analysis/MutuallyUnbiased/MixedSemantics
5649 -
lean
ClassicalBase.lean
in lean/OAI/Analysis/AncientFlat/Kernel
5640 -
lean
CertificatesK7.lean
in lean/OAI/Combinatorics/Ramsey/CycleClique/Construction
5622 -
lean
CoverageK11.lean
in lean/OAI/Combinatorics/Ramsey/CycleClique/Construction
5619 -
lean
GeodesicGeometry12.lean
in lean/OAI/Geometry/EinsteinFour
5516 -
tex
glyphtounicode.tex
in preprints/The-Falconer-distance-conjecture-in-all-dimensions-September-23-2026/build
5505 -
tex
glyphtounicode.tex
in preprints/The-spacetime-Penrose-inequality-with-charge-and-original-data-rigidity-October-5-2026/build
5505 -
lean
Sources77.lean
in lean/OAI/Analysis/MutuallyUnbiased/MixedSemantics
5496 -
lean
Roots.lean
in lean/OAI/Analysis/PlanarPacking
5409 -
lean
HighMoments1_1.lean
in lean/OAI/Analysis/PlanarPacking/Certificate
5388 -
lean
HighMoments0_5.lean
in lean/OAI/Analysis/PlanarPacking/Certificate
5388 -
lean
HighMoments3_0.lean
in lean/OAI/Analysis/PlanarPacking/Certificate
5388 -
lean
HighMoments0_4.lean
in lean/OAI/Analysis/PlanarPacking/Certificate
5388 -
lean
HighMoments1_0.lean
in lean/OAI/Analysis/PlanarPacking/Certificate
5388 -
lean
HighMoments0_2.lean
in lean/OAI/Analysis/PlanarPacking/Certificate
5388 -
lean
HighMoments1_6.lean
in lean/OAI/Analysis/PlanarPacking/Certificate
5388 -
lean
HighMoments0_1.lean
in lean/OAI/Analysis/PlanarPacking/Certificate
5388 -
lean
HighMoments1_5.lean
in lean/OAI/Analysis/PlanarPacking/Certificate
5388 -
lean
HighMoments1_4.lean
in lean/OAI/Analysis/PlanarPacking/Certificate
5388 -
lean
HighMoments0_0.lean
in lean/OAI/Analysis/PlanarPacking/Certificate
5388 -
lean
HighMoments1_2.lean
in lean/OAI/Analysis/PlanarPacking/Certificate
5388 -
lean
HighMoments0_6.lean
in lean/OAI/Analysis/PlanarPacking/Certificate
5388 -
lean
Sources75.lean
in lean/OAI/Analysis/MutuallyUnbiased/MixedSemantics
5363 -
lean
SeedContraction.lean
in lean/OAI/Topology/EilenbergGanea
5350 -
lean
Model.lean
in lean/OAI/InformationTheory/SecretKey
5319 -
lean
ClosedWords.lean
in lean/OAI/Algebra/GroupRing
5278 -
lean
Sources73.lean
in lean/OAI/Analysis/MutuallyUnbiased/MixedSemantics
5246 -
lean
Sources19.lean
in lean/OAI/Analysis/MutuallyUnbiased/MixedSemantics
5204 -
lean
Sources32.lean
in lean/OAI/Analysis/MutuallyUnbiased/MixedSemantics
5068 -
tex
manuscript.tex
in preprints/Global-Arthur-Enhancements-of-Cuspidal-Excursion-Parameters-October-5-2026/build
5019 -
tex
paper.tex
in preprints/Algebraic-Kuga-Satake-correspondences-and-Hodge-conjectures-on-a-K3-quadratic-locus-September-30-2026/build
4969 -
tex
manuscript.tex
in preprints/Algebraicity-of-Kuga-Satake-Correspondences-for-K3-Surfaces-October-3-2026/build
4929 -
lean
Sources78.lean
in lean/OAI/Analysis/MutuallyUnbiased/MixedSemantics
4834 -
lean
Canonical154.lean
in lean/OAI/Analysis/MutuallyUnbiased/MixedSemantics
4829 -
lean
Sources79.lean
in lean/OAI/Analysis/MutuallyUnbiased/MixedSemantics
4803 -
Files With Most Units (Top 50)
File# lines# units
check_certificate.py
in preprints/An-atomic-certificate-for-triangular-lattice-universal-optimality-September-26-2026/verification
364 60
exact-source.py
in preprints/The-critical-dimension-for-one-phase-Bernoulli-minimizers-September-24-2026/verification/checks/original/checks
385 59
appendix-a.cpp
in preprints/Foulkes-Conjecture-for-the-Sixth-Symmetric-Power-September-25-2026/verification/programs
699 56
verify.py
in preprints/Exact-Fourier-certificates-for-complex-Hadamard-matrices-of-order-six-September-24-2026/verification
542 51
core.hpp
in preprints/Triangular-minimality-for-planar-Coulomb-renormalized-energy-September-23-2026/verification
289 49
menu.hpp
in preprints/Complex-Matrix-Multiplication-Below-2.258-and-Rectangular-Bounds-September-24-2026/verification/certificate/checkers
212 39
exact_verifier.py
in preprints/Stable-Self-Similar-Blowup-for-a-Supercritical-Defocusing-Schrodinger-Equation-on-the-Torus-September-24-2026/verification/certificates
352 34
verify_scalar.py
in preprints/A-sharp-entropy-bound-and-the-simplex-inequality-for-isotropic-constants-October-5-2026/verification
372 32
interval_certificate.cpp
in preprints/Hellinger-contraction-with-arbitrary-Boolean-output-bias-September-24-2026/verification
201 32
interval.cpp
in preprints/The-exact-reconstruction-threshold-for-the-three-state-symmetric-channel-September-25-2026/verification
293 29
original_exact_certificates.py
in preprints/Stable-Self-Similar-Blowup-for-a-Supercritical-Defocusing-Schrodinger-Equation-on-the-Torus-September-24-2026/verification/certificates
198 28
polynomial.py
in preprints/Zero-Plane-Rigidity-for-Einstein-Four-Manifolds-October-4-2026/verification
228 27
polynomial.py
in preprints/Positively-curved-Einstein-four-manifolds-September-23-2026/verification
228 27
verify_degree31.py
in preprints/Arithmetic-classification-and-non-Pisot-singularity-for-Bernoulli-convolutions-October-3-2026/verification
375 26
profile_certificate.py
in preprints/Hellinger-contraction-with-arbitrary-Boolean-output-bias-September-24-2026/verification
137 25
scalar_intervals.py
in preprints/The-Mahler-Conjecture-for-General-Convex-Bodies-September-22-2026/verification/programs
148 25
ib.cpp
in preprints/Complex-Matrix-Multiplication-Below-2.258-and-Rectangular-Bounds-September-24-2026/verification/certificate/checkers
137 24
certificate.cpp
in preprints/The-Reconstruction-Threshold-for-the-Ferromagnetic-Four-State-Potts-Model-October-5-2026/verification/checks
175 23
segment-large-check.py
in preprints/The-Mahler-Conjecture-for-General-Convex-Bodies-September-22-2026/verification/programs
129 22
certificate.py
in preprints/A-finite-time-singularity-of-Calabi-flow-on-projective-space-September-24-2026/verification
136 21
reproduce.py
in preprints/The-critical-dimension-for-one-phase-Bernoulli-minimizers-September-24-2026/verification/checks
376 19
independent.py
in preprints/Snaky-in-21-Maker-moves-September-25-2026/verification/supporting/route21
218 18
check_sjj_rational.py
in preprints/A-sharp-Fourier-certificate-for-planar-circle-packing-September-23-2026/verification
177 18
engine.py
in preprints/The-critical-dimension-for-one-phase-Bernoulli-minimizers-September-24-2026/verification/independent-certificate
301 18
independent_checker.py
in preprints/Cycle-clique-Ramsey-numbers-September-25-2026/verification/code
256 17
numeric_balls.py
in preprints/Universal-optimality-of-the-triangular-lattice-September-23-2026/verification
277 17
independent_evaluator.py
in preprints/Snaky-in-21-Maker-moves-September-25-2026/verification/supporting
179 16
verify.py
in preprints/Zero-Plane-Rigidity-for-Einstein-Four-Manifolds-October-4-2026/verification
457 15
verify.py
in preprints/Positively-curved-Einstein-four-manifolds-September-23-2026/verification
457 15
smallcode_submitted.cpp
in preprints/Universal-Tensor-Squares-for-Symmetric-Groups-September-24-2026/verification/code
117 14
boundary-independent.py
in preprints/The-critical-dimension-for-one-phase-Bernoulli-minimizers-September-24-2026/verification/checks/original/checks
194 14
independent_certificate.py
in preprints/Snaky-in-21-Maker-moves-September-25-2026/verification/supporting/route25
284 13
grid.cpp
in preprints/The-exact-reconstruction-threshold-for-the-three-state-symmetric-channel-September-25-2026/verification
198 13
inputs.py
in preprints/Universal-optimality-of-the-triangular-lattice-September-23-2026/verification
226 13
exact_certificate.py
in preprints/Entanglement-with-zero-distillable-secret-key-in-local-dimension-ten-September-27-2026/verification
114 13
appendix-b.cpp
in preprints/Foulkes-Conjecture-for-the-Sixth-Symmetric-Power-September-25-2026/verification/programs
134 12
verify_computations.py
in preprints/Foulkes-Conjecture-for-the-Sixth-Symmetric-Power-September-25-2026/verification
295 12
tail-check.py
in preprints/A-finite-time-singularity-of-Calabi-flow-on-projective-space-September-24-2026/verification
149 12
grids.hpp
in preprints/Triangular-minimality-for-planar-Coulomb-renormalized-energy-September-23-2026/verification
343 12
independent_opening.py
in preprints/Snaky-in-21-Maker-moves-September-25-2026/verification/supporting/route35
270 11
verify_certificate.py
in preprints/Snaky-in-21-Maker-moves-September-25-2026/verification/supporting/route25
240 11
verify_certificate.py
in preprints/Snaky-in-21-Maker-moves-September-25-2026/verification/supporting/route35
224 10
original_checker.py
in preprints/Cycle-clique-Ramsey-numbers-September-25-2026/verification/code
162 10
original-computation.py
in preprints/The-periodic-spin-one-Haldane-gap-September-24-2026/verification/computations/source1
156 10
verify.py
in preprints/The-Campana-Peternell-conjecture-in-dimension-six-September-25-2026/verification
159 10
independent_certificate.py
in preprints/Snaky-in-21-Maker-moves-September-25-2026/verification/supporting/route35
185 9
smallcode_verify.py
in preprints/Universal-Tensor-Squares-for-Symmetric-Groups-September-24-2026/verification/code
200 9
verify_parameters.py
in preprints/Staggered-extraction-for-exact-matrix-multiplication-over-every-field-September-24-2026/verification/scripts
472 9
packed_lanes_independent_check.py
in preprints/The-periodic-spin-one-Haldane-gap-September-24-2026/verification/computations/source2
154 9
audit_arithmetic.py
in preprints/The-periodic-spin-one-Haldane-gap-September-24-2026/verification/computations/source2
131 9
Files With Long Lines (Top 50)

There are 21286 files with lines longer than 120 characters. In total, there are 692326 long lines.

File# lines# units# long lines
lean
HighMoments0_5.lean
in lean/OAI/Analysis/PlanarPacking/Certificate
5388 - 1680
lean
HighMoments0_4.lean
in lean/OAI/Analysis/PlanarPacking/Certificate
5388 - 1680
lean
HighMoments1_5.lean
in lean/OAI/Analysis/PlanarPacking/Certificate
5388 - 1680
lean
HighMoments1_4.lean
in lean/OAI/Analysis/PlanarPacking/Certificate
5388 - 1680
lean
HighMoments0_6.lean
in lean/OAI/Analysis/PlanarPacking/Certificate
5388 - 1672
lean
HighMoments1_6.lean
in lean/OAI/Analysis/PlanarPacking/Certificate
5388 - 1671
lean
HighMoments3_0.lean
in lean/OAI/Analysis/PlanarPacking/Certificate
5388 - 1664
lean
HighMoments1_0.lean
in lean/OAI/Analysis/PlanarPacking/Certificate
5388 - 1664
lean
HighMoments0_0.lean
in lean/OAI/Analysis/PlanarPacking/Certificate
5388 - 1662
lean
CertificatesK7.lean
in lean/OAI/Combinatorics/Ramsey/CycleClique/Construction
5622 - 1568
lean
HighMoments0_1.lean
in lean/OAI/Analysis/PlanarPacking/Certificate
5388 - 1403
lean
HighMoments1_1.lean
in lean/OAI/Analysis/PlanarPacking/Certificate
5388 - 1395
lean
WaveIntervals.lean
in lean/OAI/Analysis/Triangular/Certificate
3821 - 1360
lean
LowBlock3_11.lean
in lean/OAI/Analysis/PlanarPacking/Certificate
4044 - 1260
lean
LowBlock3_10.lean
in lean/OAI/Analysis/PlanarPacking/Certificate
4044 - 1259
lean
LowBlock9_0.lean
in lean/OAI/Analysis/PlanarPacking/Certificate
4044 - 1245
lean
LowBlock12_0.lean
in lean/OAI/Analysis/PlanarPacking/Certificate
4044 - 1245
lean
LowBlock7_0.lean
in lean/OAI/Analysis/PlanarPacking/Certificate
4044 - 1244
lean
LowBlock33_0.lean
in lean/OAI/Analysis/PlanarPacking/Certificate
4044 - 1244
lean
LowBlock15_0.lean
in lean/OAI/Analysis/PlanarPacking/Certificate
4044 - 1244
lean
LowBlock31_0.lean
in lean/OAI/Analysis/PlanarPacking/Certificate
4044 - 1244
lean
LowBlock37_0.lean
in lean/OAI/Analysis/PlanarPacking/Certificate
4044 - 1244
lean
LowBlock13_0.lean
in lean/OAI/Analysis/PlanarPacking/Certificate
4044 - 1244
lean
LowBlock16_0.lean
in lean/OAI/Analysis/PlanarPacking/Certificate
4044 - 1244
lean
LowBlock4_0.lean
in lean/OAI/Analysis/PlanarPacking/Certificate
4044 - 1244
lean
LowBlock36_0.lean
in lean/OAI/Analysis/PlanarPacking/Certificate
4044 - 1244
lean
LowBlock21_0.lean
in lean/OAI/Analysis/PlanarPacking/Certificate
4044 - 1243
lean
LowBlock19_0.lean
in lean/OAI/Analysis/PlanarPacking/Certificate
4044 - 1243
lean
LowBlock40_0.lean
in lean/OAI/Analysis/PlanarPacking/Certificate
4044 - 1243
lean
LowBlock27_0.lean
in lean/OAI/Analysis/PlanarPacking/Certificate
4044 - 1243
lean
LowBlock39_0.lean
in lean/OAI/Analysis/PlanarPacking/Certificate
4044 - 1243
lean
LowBlock25_0.lean
in lean/OAI/Analysis/PlanarPacking/Certificate
4044 - 1243
lean
LowBlock24_0.lean
in lean/OAI/Analysis/PlanarPacking/Certificate
4044 - 1243
lean
LowBlock28_0.lean
in lean/OAI/Analysis/PlanarPacking/Certificate
4044 - 1243
lean
HighMoments0_7.lean
in lean/OAI/Analysis/PlanarPacking/Certificate
4716 - 1204
lean
UMoments19.lean
in lean/OAI/Analysis/PlanarPacking/Certificate
3924 - 1171
lean
UMoments21.lean
in lean/OAI/Analysis/PlanarPacking/Certificate
3924 - 1171
lean
UMoments7.lean
in lean/OAI/Analysis/PlanarPacking/Certificate
3924 - 1170
lean
UMoments31.lean
in lean/OAI/Analysis/PlanarPacking/Certificate
3924 - 1169
lean
UMoments67.lean
in lean/OAI/Analysis/PlanarPacking/Certificate
3924 - 1168
lean
UMoments45.lean
in lean/OAI/Analysis/PlanarPacking/Certificate
3924 - 1167
lean
UMoments33.lean
in lean/OAI/Analysis/PlanarPacking/Certificate
3924 - 1166
lean
UMoments9.lean
in lean/OAI/Analysis/PlanarPacking/Certificate
3924 - 1166
lean
UMoments55.lean
in lean/OAI/Analysis/PlanarPacking/Certificate
3924 - 1165
lean
UMoments57.lean
in lean/OAI/Analysis/PlanarPacking/Certificate
3924 - 1165
lean
UMoments79.lean
in lean/OAI/Analysis/PlanarPacking/Certificate
3924 - 1164
lean
UMoments40.lean
in lean/OAI/Analysis/PlanarPacking/Certificate
3924 - 1164
lean
UMoments43.lean
in lean/OAI/Analysis/PlanarPacking/Certificate
3924 - 1163
lean
UMoments64.lean
in lean/OAI/Analysis/PlanarPacking/Certificate
3924 - 1162
lean
UMoments91.lean
in lean/OAI/Analysis/PlanarPacking/Certificate
3924 - 1162
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...