Will aesop be able to replace >50% of mathlib proofs by 2025-11-26?
18
1kṀ498
Nov 26
41%
chance

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
to start trading!
© Manifold Markets, Inc.TermsPrivacy