Will Kevin Buzzard successfully fulfill his grant specs of formalizing Fermat's Last Theorem in Lean within 5 years?

Prediction market on manifold. Grant specs: https://gow.epsrc.ukri.org/NGBOViewGrant.aspx?GrantRef=EP/Y022904/1

24h Volume: $200. Liquidity: $1,000. Resolves: 1/1/2031.