openai / miniF2F
File Size

The distribution of size of files (measured in lines of code).

Intro
Learn more...
File Size Overall
21% | 0% | 2% | 0% | 76%
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
lean96% | 0% | 0% | 0% | 3%
py0% | 0% | 100% | 0% | 0%
thy0% | 0% | 0% | 0% | 100%
mm0% | 0% | 0% | 0% | 100%
ml0% | 0% | 0% | 0% | 100%
toml0% | 0% | 0% | 0% | 100%
File Size per Logical Decomposition
primary
1001+
501-1000
201-500
101-200
1-100
lean86% | 0% | 9% | 0% | 3%
isabelle0% | 0% | 0% | 0% | 100%
metamath0% | 0% | 0% | 0% | 100%
hollight0% | 0% | 0% | 0% | 100%
ROOT0% | 0% | 0% | 0% | 100%
Longest Files (Top 50)
File# lines# units
lean
valid.lean
in lean/src
 2132 -
lint_style.py
in lean/scripts
 234 15
lean
 87 -
76 -
amc12b-2004-p3.mm
in metamath/valid
 53 -
induction-seq-mul2pnp1.mm
in metamath/valid
 51 -
46 -
thy
 44 -
amc12b-2003-p6.mm
in metamath/valid
 43 -
43 -
mathd-algebra-31.mm
in metamath/valid
 40 -
induction-sum-1oktkp1.mm
in metamath/valid
 40 -
37 -
37 -
amc12b-2003-p9.mm
in metamath/valid
 36 -
mathd-algebra-245.mm
in metamath/valid
 36 -
thy
mathd_algebra_245.thy
in isabelle/valid
 36 -
thy
amc12a_2003_p24.thy
in isabelle/valid
 35 -
34 -
amc12b-2002-p3.mm
in metamath/valid
 34 -
mathd-algebra-159.mm
in metamath/valid
 34 -
33 -
32 -
31 -
amc12a-2003-p24.mm
in metamath/valid
 31 -
31 -
thy
amc12b_2002_p3.thy
in isabelle/valid
 31 -
amc12-2000-p11.mm
in metamath/valid
 29 -
thy
amc12a_2013_p8.thy
in isabelle/valid
 29 -
mathd-algebra-151.mm
in metamath/valid
 28 -
amc12-2001-p9.mm
in metamath/valid
 28 -
induction-sum-odd.mm
in metamath/valid
 28 -
amc12b-2003-p17.mm
in metamath/valid
 27 -
thy
mathd_algebra_405.thy
in isabelle/valid
 27 -
thy
mathd_algebra_11.thy
in isabelle/valid
 26 -
amc12a-2003-p1.mm
in metamath/valid
 25 -
25 -
25 -
25 -
thy
mathd_algebra_101.thy
in isabelle/valid
 25 -
thy
mathd_algebra_422.thy
in isabelle/valid
 25 -
ml
aime-1984-p15.ml
in hollight/valid
 24 -
thy
aime_1983_p9.thy
in isabelle/valid
 24 -
thy
mathd_algebra_132.thy
in isabelle/valid
 24 -
24 -
mathd-algebra-192.mm
in metamath/valid
 23 -
23 -
23 -
thy
amc12a_2003_p1.thy
in isabelle/valid
 23 -
thy
amc12b_2003_p17.thy
in isabelle/valid
 22 -
Files With Most Units (Top 1)
File# lines# units
lint_style.py
in lean/scripts
 234 15
Files With Long Lines (Top 50)

There are 59 files with lines longer than 120 characters. In total, there are 79 long lines.

File# lines# units# long lines
lean
valid.lean
in lean/src
 2132 - 5
imo-1966-p5.mm
in metamath/valid
 19 - 5
aime-1984-p15.mm
in metamath/valid
 15 - 4
ml
amc12b-2021-p21.ml
in hollight/valid
 5 - 3
amc12a-2002-p21.mm
in metamath/valid
 11 - 2
11 - 2
aimeII-2020-p6.mm
in metamath/valid
 13 - 2
imo-1965-p1.mm
in metamath/valid
 12 - 2
imo-1962-p4.mm
in metamath/valid
 9 - 2
amc12a-2019-p9.mm
in metamath/valid
 11 - 2
ml
mathd-numbertheory-690.ml
in hollight/valid
 8 - 2
aime-1983-p9.mm
in metamath/valid
 9 - 1
mathd-numbertheory-403.mm
in metamath/valid
 7 - 1
7 - 1
imo-1993-p5.mm
in metamath/valid
 7 - 1
mathd-numbertheory-640.mm
in metamath/valid
 7 - 1
imo-1977-p5.mm
in metamath/valid
 14 - 1
amc12a-2016-p3.mm
in metamath/valid
 9 - 1
mathd-algebra-10.mm
in metamath/valid
 7 - 1
mathd-numbertheory-269.mm
in metamath/valid
 7 - 1
aime-1988-p4.mm
in metamath/valid
 11 - 1
amc12a-2010-p10.mm
in metamath/valid
 15 - 1
imo-1967-p3.mm
in metamath/valid
 13 - 1
mathd-algebra-89.mm
in metamath/valid
 8 - 1
imo-1974-p5.mm
in metamath/valid
 13 - 1
mathd-algebra-568.mm
in metamath/valid
 8 - 1
mathd-numbertheory-303.mm
in metamath/valid
 7 - 1
mathd-algebra-509.mm
in metamath/valid
 7 - 1
mathd-algebra-140.mm
in metamath/valid
 12 - 1
aime-1997-p12.mm
in metamath/valid
 9 - 1
aimeI-2001-p3.mm
in metamath/valid
 15 - 1
amc12a-2020-p13.mm
in metamath/valid
 16 - 1
mathd-numbertheory-126.mm
in metamath/valid
 12 - 1
mathd-numbertheory-221.mm
in metamath/valid
 7 - 1
aime-1990-p2.mm
in metamath/valid
 7 - 1
mathd-numbertheory-30.mm
in metamath/valid
 7 - 1
mathd-algebra-282.mm
in metamath/valid
 10 - 1
11 - 1
amc12b-2021-p21.mm
in metamath/valid
 8 - 1
10 - 1
mathd-numbertheory-405.mm
in metamath/valid
 17 - 1
mathd-algebra-13.mm
in metamath/valid
 10 - 1
imo-2006-p6.mm
in metamath/valid
 10 - 1
amc12a-2009-p25.mm
in metamath/valid
 11 - 1
8 - 1
mathd-numbertheory-149.mm
in metamath/valid
 7 - 1
imo-1973-p3.mm
in metamath/valid
 10 - 1
imo-1966-p4.mm
in metamath/valid
 10 - 1
amc12a-2019-p21.mm
in metamath/valid
 9 - 1
1 - 1
Correlations

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

lean/src/valid.lean x: 36 commits (all time) y: 2132 lines of code lean/src/minif2f_import.lean x: 15 commits (all time) y: 87 lines of code leanpkg.toml x: 14 commits (all time) y: 7 lines of code isabelle/valid/mathd_algebra_96.thy x: 3 commits (all time) y: 15 lines of code isabelle/valid/aime_1991_p6.thy x: 4 commits (all time) y: 13 lines of code isabelle/valid/imo_1967_p3.thy x: 5 commits (all time) y: 16 lines of code isabelle/valid/mathd_algebra_101.thy x: 5 commits (all time) y: 25 lines of code isabelle/valid/aime_1990_p2.thy x: 2 commits (all time) y: 11 lines of code hollight/valid/mathd-numbertheory-301.ml x: 4 commits (all time) y: 5 lines of code isabelle/valid/aimeI_2000_p7.thy x: 2 commits (all time) y: 19 lines of code isabelle/valid/mathd_numbertheory_13.thy x: 4 commits (all time) y: 18 lines of code hollight/valid/mathd-algebra-131.ml x: 5 commits (all time) y: 8 lines of code isabelle/valid/aime_1996_p5.thy x: 3 commits (all time) y: 20 lines of code isabelle/valid/amc12a_2013_p8.thy x: 3 commits (all time) y: 29 lines of code isabelle/valid/mathd_algebra_245.thy x: 3 commits (all time) y: 36 lines of code metamath/valid/mathd-algebra-131.mm x: 6 commits (all time) y: 13 lines of code hollight/valid/aime-1983-p9.ml x: 2 commits (all time) y: 3 lines of code metamath/valid/aimeI-2001-p3.mm x: 1 commits (all time) y: 15 lines of code metamath/valid/aime-1990-p2.mm x: 1 commits (all time) y: 7 lines of code metamath/valid/aime-1996-p5.mm x: 1 commits (all time) y: 21 lines of code lean/scripts/lint_style.py x: 1 commits (all time) y: 234 lines of code isabelle/valid/amc12a_2003_p24.thy x: 1 commits (all time) y: 35 lines of code isabelle/valid/amc12b_2002_p3.thy x: 1 commits (all time) y: 31 lines of code isabelle/valid/induction_ineq_nsqlefactn.thy x: 1 commits (all time) y: 44 lines of code metamath/valid/algebra-2varlineareq-xpeeq7-2xpeeq3-eeq11-xeqn4.mm x: 2 commits (all time) y: 31 lines of code metamath/valid/algebra-amgm-faxinrrp2msqrt2geq2mxm1div2x.mm x: 3 commits (all time) y: 7 lines of code metamath/valid/amc12b-2002-p3.mm x: 2 commits (all time) y: 34 lines of code metamath/valid/amc12b-2003-p6.mm x: 2 commits (all time) y: 43 lines of code metamath/valid/amc12b-2004-p3.mm x: 3 commits (all time) y: 53 lines of code metamath/valid/induction-seq-mul2pnp1.mm x: 2 commits (all time) y: 51 lines of code metamath/valid/numbertheory-prmdvsneqnsqmodpeq0.mm x: 2 commits (all time) y: 76 lines of code
2132.0
lines of code
  min: 1.0
  average: 15.24
  25th percentile: 7.0
  median: 11.0
  75th percentile: 14.0
  max: 2132.0
0 36.0
commits (all time)
min: 1.0 | average: 2.33 | 25th percentile: 2.0 | median: 2.0 | 75th percentile: 3.0 | max: 36.0

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

lean/src/valid.lean x: 6 contributors (all time) y: 2132 lines of code lean/src/minif2f_import.lean x: 4 contributors (all time) y: 87 lines of code leanpkg.toml x: 2 contributors (all time) y: 7 lines of code isabelle/valid/mathd_algebra_96.thy x: 2 contributors (all time) y: 15 lines of code isabelle/valid/imo_1967_p3.thy x: 3 contributors (all time) y: 16 lines of code isabelle/valid/mathd_algebra_101.thy x: 3 contributors (all time) y: 25 lines of code hollight/valid/mathd-numbertheory-301.ml x: 3 contributors (all time) y: 5 lines of code isabelle/valid/aimeI_2000_p7.thy x: 2 contributors (all time) y: 19 lines of code hollight/valid/mathd-algebra-131.ml x: 4 contributors (all time) y: 8 lines of code isabelle/valid/amc12a_2013_p8.thy x: 3 contributors (all time) y: 29 lines of code isabelle/valid/mathd_algebra_245.thy x: 3 contributors (all time) y: 36 lines of code metamath/valid/amc12a-2013-p8.mm x: 4 contributors (all time) y: 13 lines of code metamath/valid/aimeI-2001-p3.mm x: 1 contributors (all time) y: 15 lines of code metamath/valid/mathd-algebra-493.mm x: 1 contributors (all time) y: 8 lines of code metamath/valid/aime-1996-p5.mm x: 1 contributors (all time) y: 21 lines of code lean/scripts/lint_style.py x: 1 contributors (all time) y: 234 lines of code isabelle/valid/amc12a_2003_p24.thy x: 1 contributors (all time) y: 35 lines of code isabelle/valid/amc12b_2002_p3.thy x: 1 contributors (all time) y: 31 lines of code isabelle/valid/induction_ineq_nsqlefactn.thy x: 1 contributors (all time) y: 44 lines of code metamath/valid/algebra-2varlineareq-xpeeq7-2xpeeq3-eeq11-xeqn4.mm x: 2 contributors (all time) y: 31 lines of code metamath/valid/algebra-sqineq-4bap1lt4bsqpap1sq.mm x: 2 contributors (all time) y: 34 lines of code metamath/valid/amc12b-2003-p6.mm x: 2 contributors (all time) y: 43 lines of code metamath/valid/amc12b-2004-p3.mm x: 2 contributors (all time) y: 53 lines of code metamath/valid/numbertheory-prmdvsneqnsqmodpeq0.mm x: 2 contributors (all time) y: 76 lines of code
2132.0
lines of code
  min: 1.0
  average: 15.24
  25th percentile: 7.0
  median: 11.0
  75th percentile: 14.0
  max: 2132.0
0 6.0
contributors (all time)
min: 1.0 | average: 2.02 | 25th percentile: 2.0 | median: 2.0 | 75th percentile: 3.0 | max: 6.0

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

No data for "commits (30d)" vs. "lines of code".

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

No data for "contributors (30d)" vs. "lines of code".

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

No data for "commits (90d)" vs. "lines of code".

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

No data for "contributors (90d)" vs. "lines of code".