

Would an AI be able to construct an ultra-weak proof for the given chess board state, that does not rely on brute-force analysis by 2030. The proof can contain multiple conditions but should not outline every move to conclude the solution.
Since the line for how many conditions is too much is subjective, I'll say that I'd be satisfied if the compressed size of the proof is < 7kb (excluding definitions+axioms)
https://en.wikipedia.org/wiki/Solved_game
https://en.wikipedia.org/wiki/Solving_chess
Bonus: 50k bounty to anyone who can manually construct a proof, its still unclear to me what would be a reasonable size for such a problem.
Update 2025-05-06 (PST) (AI summary of creator comment): - For the chess board state relevant to this market, it is confirmed that castling by either side is allowed.
@CollinMatthews
Castling is allowed.
It should be rigorous enough to translate into a theorem prover like Lean/Coq