mechanical definition of "proof complexity"

Stream: new members

[Rado Kirov]

(this is a very hand-wavy thought and not a real question, hope it is ok for this forum)

I just finished chapter 4 of MIL and was thinking about Shroeder-Bernstein being the first example of notably harder proof than anything done earlier. Made me wonder if someone has thought about defining a syntactically computable measure of "proof complexity". Shroeder-Bernstein's theorem needs a mini-insight in defining sbFun while all other theorems are just "follow your nose".

Something akin to https://en.wikipedia.org/wiki/Cyclomatic_complexity in computational programs. Similarly to cyclomatic_complexity, this would be heuristic and "game-able", but still can be cool to run over mathlib to point out where the "strokes of insights" lie .

A first approximation could be lines of Lean, or maybe number of new definitions. Has anyone looked into something like this before?

[Bjørn Kjos-Hanssen]

Lines of code, size of libraries and general complexity of everything involved is a key challenge for formalization of mathematics at scale for sure...