Will an inconsistency in the Calculus of Inductive Constructions be found before 2050?

10

51

Ṁ888Ṁ1k

2049

4%

chance

1D

1W

1M

ALL

The Calculus of Inductive Constructions is the formal system underlying the Coq proof assistant (see https://coq.github.io/doc/v8.9/refman/language/cic.html).

This will resolve to YES if a proof of a contradiction is published in a peer-reviewed scientific conference or journal on computer proof assistants or a similar area, such as Logic in Computer Science, or if a majority vote of at least 5 researchers in the field of computer proof assistants agree that such a result published elsewhere is correct, before the start of 2050. Otherwise, this will resolve to NO at the start of 2050.

Get Ṁ600 play money

Sort by:

## More related questions

## Related questions

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

67% chance

Conditional on no existential catastrophe, will there be a superintelligence by 2050?

47% chance

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

21% chance

Will we have a formalized proof of Fermat's last theorem by 2029-05-01?

61% chance

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

50% chance

Will ZFC no longer be the standard foundation for mathematics by 2050?

34% chance

Will we have a proof of the Riemann Hypothesis by 2060?

46% chance

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

65% chance

Will Goldbach's conjecture be proved before 2040?

36% chance

Will consequential atomically precise manufacturing systems be developed before 2040?

40% chance