[deterministic]

> someone wins a Fields using a proof-assistant in an essential way.

Terence Tao is actively using LEAN and working with the LEAN community to prove leading edge mathematics.