Theorem proving olympiad

Stream: Machine Learning for Theorem Proving

[(deleted)]

Looks like we keep celebrating AI progress in theorem proving. But a crucial question is whether AI can be as fast as humans. I have a feeling that if a person memorizes mathlib lemma names and is fluent enough in Lean, they can surpass AI in speed and success rate. This should be put to a test.

[(deleted)]

I feel trips to Loogle and mathlib docs are the bottleneck in many cases.

[Yan Yablonovskiy 🇺🇦]

Is efficiency of the proof scored at all? If so , then I definitely agree.

[(deleted)]

The proof must compile in less than 1 minute. Aside from that, the compilation time is not part of the scoring criteria.

[(deleted)]

However, the time needed to come up with the proof is the main scoring criterion.

[(deleted)]

I figured that the processing speed of Lean also affects how fast a human can be

[Bas Spitters]

Caterine Lelay did something similar in Rocq in 2014:
https://jfla.inria.fr/2014/lelay.pdf

"Le bac" is the common, shortened name for "le baccalauréat", which is the national examination that French students take at the end of their secondary education (high school). It is a major rite of passage and is required for students to continue their studies at a university.

[Jason Rute]

There used to be competitions in ITP, right?

[Jason Rute]

This: https://www21.in.tum.de/%7Ewimmers/proofground/

[Jason Rute]

Using this contest system: https://do.proof.in.tum.de