Will the majority of mathematicians rely on formal computer proof assistants before the end of 2040?
32
1kṀ1333
2040
60%
chance

Computer proof assistant is a tool, that by using computation, is able with "certainty", verify and build new proofs from underlying specified axioms (Lean4, Coq, Agda, etc...).

Resolves YES if before the end of 2040 there is a trustworthy poll/evidence that shows more than 50% of professional mathematicians use or rely on it.

Get
Ṁ1,000
to start trading!
© Manifold Markets, Inc.TermsPrivacy