Will rw_search be able to replace >50% of mathlib proofs by 2025-11-26?
Basic
9
Ṁ280
2025
19%
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 rw_search.

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

Get
Ṁ1,000
and
S3.00
© Manifold Markets, Inc.Terms + Mana-only TermsPrivacyRules