- On March 14, 2024, I bet Ɖ100 of my money against Ɖ100 of Yunchao Liu’s that a resolution of $\text{TC}^0$ vs $\text{NEXP}$ will not be proved by an automated theorem prover or AI system by March 14, 2029. The bet will resolve in my favor if (1) the status of TC0 vs NEXP were to be unknown; or (2) human researcher(s) were to solve the problem, by that date. It will resolve in Yunchao’s favor otherwise. A combination of human and AI proof, for example, via a human researcher prompting and revising a language model’s outputs, will resolve the bet as ambiguous. Winner: TBD.