Он выложил предварительный код формального доказательства на Lean4 (из России топовые математики без винни-пуха недоступны), и забился на 10k баксов с профессором Маркусом Хаттером (автор AIXI, теоретической модели универсального агента).
Но сам приз так-то миллион долларов, ставки делают, правда 98% не верят что получится, и я тоже:)
Но хайпанул пацан чётко. не ну а чо.
THE PROOF IS COMPLETE.
All logical steps are formalized. The theorem `navier_stokes_regularity` proves:
For any NS solution satisfying the physical axioms, blowup is impossible.
The physical axioms are:
1. Type II exponent α > 1 (from ESS theorem)
2. Spectral gap νP ≥ c•Ω•E (from Poincaré on dissipation scale)
3. θ dynamics S ≤ C•(T-t)^{α-1}•Ω•E (from alignment ODE)
4. Blowup rate Ω ≤ C•(T-t)^{-α} (from Type II characterization)
5. BKM criterion (from Agmon interpolation)
Each axiom is verified from NS physics in the accompanying theorems.
А я только три дня назад эту идею спалил =>
"Идея для math-стартапа: перевОдите это (и другие подобные от топовых математиков) доказательство в формальный вид на теорем-прувере вроде Lean или Coq, и получаете реальную мировую известность."
Дэвид, раз читаешь мой блог, задонать сотку баксов :)