Will aesop be able to replace >50% of mathlib proofs by 2025-11-26?

Basic

17

Ṁ4942025

40%

chance

1D

1W

1M

ALL

Sometime around the resolution date, I will write a script that samples random tactic-mode lemmas from mathlib, and replaces the proof of those lemmas with an invocation of aesop.

Resolves YES if aesop successfully proves >50% of the lemmas.

Get Ṁ1,000 play money

Sort by:

You will use `aesop`

without any arguments or additional configuration (besides what is given in mathlib)?

## Related questions

## Related questions

Will an AI get gold on any International Math Olympiad by the end of 2025?

71% chance

Will rw_search be able to replace >50% of mathlib proofs by 2025-11-26?

19% chance

Will any AI be able to explain formal language proofs to >=50% of IMO problems by the start of 2025?

48% chance

In 2029, will any AI be able to take an arbitrary proof in the mathematical literature and translate it into a form suitable for symbolic verification? (Gary Marcus benchmark #5)

61% chance

Will AIs be widely recognized as having developed a new, innovative, foundational mathematical theory before 2030?

31% chance

Will an AI solve any important mathematical conjecture before January 1st, 2030?

76% chance

Will an AI be able to convert recent mathematical results into a fully formal proofs that can be verified by a mainstream proof assistant by 2025?

18% chance

Will an AI get bronze or silver on any International Math Olympiad by end of 2025?

72% chance

Will the majority of mathematicians rely on formal computer proof assistants before the end of 2040?

71% chance

Will reinforcement learning overtake LMs on math before 2028?

57% chance