Will the majority of mathematicians rely on formal computer proof assistants before the end of 2040?
➕
Plus
32
Ṁ1125
2040
69%
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.

#️ Technology
#Mathematics
Get
Ṁ1,000
and
S3.00
6 Comments
29 Holders
53 Trades
Sort by:

How will this question resolve if AI becomes significantly stronger than human mathematicians at math and therefore the nature of the profession is transformed in some way?

@OlegEterevsky For example, what if mathematicians will primarily do teaching, rather than research?

predicts YES

@OlegEterevsky As long as the word "relying on" makes sense...

predicts YES

@OlegEterevsky So teaching but utilizing proof assistants would qualify.

I think it would happen but nobody’s actually going to conduct a randomly sampled poll on this.

predicts YES

@thepurplebull I've added "trustworthy evidence" as also a resolution qualifier.

Related questions

© Manifold Markets, Inc.•Terms + Mana-only Terms•Privacy•Rules