Resolved by a successful solution accepted at https://lean-lang.org/eval/problems/jacobian_challenge_alggeo/
Update 2026-05-29 (PST) (AI summary of creator comment): - The creator is the maintainer of the lean-eval and will audit submissions before resolving
If a submission hacks the eval (e.g., proves False by the same technique), the market will not resolve YES
The creator intends to participate in this market but will stop trading after any submission is received
1,000(Note that I'm the maintainer of the lean-eval. I will only resolve this market after auditing a successful submission, and in particular if the submission manages to hack the eval -- e.g. the submitter could have proved False by the same technique -- I will not resolve this market.
I intend to participate in this market, but will undertake not to after any submission is received.)