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.