Tooling for handling lean files en masse

[qrdlgit]

Some stats:

• number_theory 1445: tokens like Prime, divisibility, modular arithmetic.
• set_finset 817: sets and finite sets (Set, Finset, Icc, Ioo, cardinality-like operations).
• analysis_topology 661: continuity, differentiability, distance, measure, volume.
• eventual_filter 580: Lean’s Filter machinery, which expresses “eventually” or “for all sufficiently large values,” such as Filter.atTop, ∀ᶠ, and
  related notation.
• asymptotic 226: growth-rate notation like Big-O, little-o, and Theta, written as =O, =o, =Θ.
• infinitude_density 228: infinite sets or density statements.
• graph_combinatorics 207: graph constructs such as SimpleGraph.
• answer_form 95: formulations explicitly involving answer-style encodings.
• optimization_extremal 64: statements about least, greatest, infimum, supremum, or best constants.

I've created a tool which does various checks on all of the lean files. Lots of linting issues, but nothing serious.

I've worked on sanity checks for counterexamples and such, but so far nothing is popping out. Will put some more work into that.

Be great to see a lot more additions to the repo, say put in a new category of 'automated extraction'. These can be very useful for data mining, even if they aren't perfect. Ideally proper tooling could weed out the problem formulations.

[qrdlgit]

Tractability Bands for formal conjectures repo:

• 883 high: good fit for bounded automation
• 703 medium: plausible, but likely needs stronger or more specialized probes
• 452 low
• 547 very_low: poor fit for the current bounded audit style

Why are so many very_low? Mostly because asymptotic and filter-heavy formulations are hard for bounded search. For example, a theorem using both Big-O notation and Filter.atTop gets multiple penalties even if Lean normalized it cleanly.

That is why examples like:

• Erdos1054.erdos_1054.parts.i
• Erdos1092.f_asymptotic_general
• Arxiv.«1609.08688».maximalLength_le_isBigO

end up very_low: they are mathematically clean, but bad targets for brute-force or small-instance automation.