Budden's claims about Navier Stokes

Stream: new members

[Tim Freeman]

I'm new here. I would like to follow along the discussion about Budden's claims to have a Lean proof that the Navier-Stokes differential equation is well behaved, but I haven't yet discovered how to search to find the right discussion. I found a "search" box in the Android app but searching for Budden or Navier gives no results. Can someone point me to the discussion?

[Weiyi Wang]

If you don't find it in "search", likely there wasn't any. So this one is the first one, I guess

[Eric Wieser]

I think most of the discussion has been on Twitter, and in the absence of the promised Lean file I don't think there is anything particularly on-topic to discuss yet on this Zulip

[Mirek Olšák]

The common belief is that Budden is not any close to solving a Millenium problem but he is using these bold claims to drag attention to his new startup. We should appreciate that he is interested in Lean but his rhetoric is lowering his credibility.

He didn't publish any large proof but sometimes he publishes a snippet. I was puzzled by the first Lean file he published. It had so many errors I suspect no one tried to run Lean on it, I rather imagine it being a result of asking ChatGPT / Gemini: "Translate this math document into Lean".

Later, he showed he is able to produce a Lean file that compiles, on the other hand, even Budden says these are just some basic results, and I don't understand PDE's enough to have an idea how meaningful / hard to formalize this is.

[Tim Freeman]

I know that LLMs confabulate, but Gemini's claim that the discussion is around here somewhere is the most persistent and wrong statement I can recall getting from it. Usually when an LLM confabulates, if you make another thread and ask again, it will confabulate differently, but not this time.

Thanks for the X/Twitter thread. I will check it out.

[Tomas Skrivan]

Who is this guy? It seems to me that people take him more seriously than any other random person that just lazily asks LLM to solve some unsolved math problem. To me, he sounds like any other crank.

[Kevin Buzzard]

(deleting double-post)

[Kevin Buzzard]

I think that what happened was that Budden was once associated with DeepMind and it was known that DeepMind were thinking about Navier-Stokes, so at the very beginning of the saga there was some extra credence coming from this connection, but it all fell apart within a few hours and ever since then it's been nothing but noise which seems to be dragging on and on (to my dismay I was even contacted by a journalist about this farce today). For me it was all over on day 1 when he posted some Lean code which didn't compile as evidence that he was onto something.

[Alex Kontorovich]

I simply refuse to engage with this stuff on Twitter (and ignore journalist requests). Is this a mistake? I'm hoping it'll go away on its own and I don't need to waste my time on it. I still think that's the right approach, in the long run...(?)

[Matthew Coke]

@Alex Kontorovich all beings are coherent to some degree, so there's undoubtedly something to learn from it, but if it's a large problem like a Millenium problem that's a relatively large hill to climb and one can certainly get lost, mistime stuff, fall for delusions, etc along the way

[Eric Wieser]

Kevin Buzzard said:

I think that what happened was that Budden was once associated with DeepMind and it was known that DeepMind were thinking about Navier-Stokes

Note that Budden is not on the related GDM paper about unstable singularities.

[Eric Wieser]

In this particular case it seems plausible that engaging with Budden at the right time could net a $10k reward (or at least a $1k charity donation), even if academically it is a poor use of time.

[Eric Vergo]

Alex Kontorovich said:

I'm hoping it'll go away on its own and I don't need to waste my time on it.

I'm guessing this will go away eventually, but not all problems do. The problems where a lot of people hope it'll go away but don't (or hope it isn't actually a problem and then it suddenly becomes one) tend to hit pretty hard.

[Tomas Skrivan]

Ok I got interested in this spectacle a bit :see_no_evil: he claims that he uses this formalization of NS problem https://github.com/lean-dojo/LeanMillenniumPrizeProblems/tree/main/Problems/NavierStokes I remember this repository being mostly AI generated and had lots of issues. Was the formulation of NS problem double checked by experts here?

Honestly, I think it is wrong. For example, Solution.T is a real number and the statement for existence is:

def ExistenceOfSmoothSolution (problem : MillenniumProblem) : Prop :=
  ∃ sol : SmoothSolution problem.nse, sol.T = (⊤ : WithTop ℝ)

Which would require that Solution.T is WithTop ℝ but it is not so you just get cast from ℝ to WithTop ℝ on lhs and the equality can't ever hold. Therefore it should be trivial to show that ExistenceOfSmoothSolution implies False.

Also I don't see a condition on Solution.domain, so you can again cheat by setting domain to an empty set ... well everything is sort of broken as the author of the repository is incorrectly using default values for struct fields, not realizing that you can set the field values to what ever you want.

[Tomas Skrivan]

(I'm on mobile right now so I can't create a proof of (forall p. ExistanceOfSmoothSolution p) -> False right now, could be fun to see his reaction to it :)

[Timothy Chow]

While it might be questionable ethically, one possibility would be offer Budden a $1 million bet that he's wrong. Since Lean is the arbiter, it should be possible to get an independent third party to settle the bet. It might also help "us" (meaning the Lean community in general) put into practice some of the things we've been talking about with regard to Lean being the arbiter of famous open problems.

[Eric Wieser]

Maybe @Robert Joseph remembers what the state of the lean-dojo statements was

[Eric Wieser]

Previous discussion was at #general > Formalization of the Millennium Prize Problems @ 💬

[Matthew Coke]

if nothing else, his effort is helping to build a list of things to not do

[Mirek Olšák]

@Tomas Skrivan you mean like this:

theorem no_smooth_solution (problem : MillenniumProblem) :
    ¬ ExistenceOfSmoothSolution problem := by
  intro h
  unfold ExistenceOfSmoothSolution at h
  obtain ⟨sol, h⟩ := h
  simp at h

#check no_smooth_solution

[Tomas Skrivan]

Yup, something like that. Is is just a mock up or does it compile?

[Mirek Olšák]

Compiles, I cloned the repository.

[Eric Wieser]

Does rintro ⟨sol, h⟩; cases h also work?

[Tomas Skrivan]

Shall we reply here https://manifold.markets/Simon74fe/outcome-of-david-buddens-navierstok#ef7hypnk24k ? :popcorn:

[Mirek Olšák]

I was rather thinking of opening a github issue in the repository, that looks more like a serious attempt to do something. I am not sure if there is a meaningful contribution to Budden's show.

[Yaël Dillies]

Does rintro ⟨sol, ⟨⟩⟩ also work?

[Tomas Skrivan]

@Mirek Olšák I guess you are right but I have a less favorable opinion of that repository. At least the NS problem(the only problem I have a reasonable capacity to check correctness of the statement) is poorly done, mostly AI generated and would require a mayor overhaul.

[Mirek Olšák]

Hm, I agree it looks weird even to me (and I haven't looked deeply & don't know about much about the topic). There is an alleged fix of NS in the history but didn't help much...

[Tomas Skrivan]

What I'm worried about that Budden posts a proof that compiles, produces pile of reasonable/complicated looking mathematics but the AI discovers this simple hack and sneaks it somewhere in the middle. All this could result in a bad image for Lean. Not sure what to do about it though

[Matthew Coke]

@Tomas Skrivan I'm abstaining, but appreciative of the popcorn

[Mirek Olšák]

I don't think it counts as a formal solution, rather as a sign that there is something really wrong about the formal statement. The formal statement is supposedly

def MillenniumProblemStatement : Prop :=
  (∀ problem : MillenniumProblem, ExistenceOfSmoothSolution problem) ∨
  (∃ problem : MillenniumProblem, BreakdownOfSmoothSolution problem)

This is weird on its own because one would intuitively expect the two branches to be negations of each other. In such case, the formal statement is a tautology (consequence of Classical.em). We have shown that the first branch simplifies to False. If the second branch is the actual milenium problem (I expect more issues but let's imagine), then proving or disproving MillenniumProblemStatement is the challenge it should be -- actually solving NS, even though phrased in a very weird way.

[Timothy Chow]

I just noticed that as far as the $10,000 bet is concerned, a crucial clause concerns uploading a paper to the arXiv in 2025. As someone who has had arXiv submissions stuck in moderation for weeks (not to mention the struggles I've sometimes had with getting an endorser for some field that I don't publish in regularly, and the stories I've heard of seemingly reasonable papers getting rejected), I wonder if the bet is going to collapse for the "silly" reason that the arXiv moderators reject the paper?

[Mirek Olšák]

Sounds plausible to me. :popcorn:

[Tomas Skrivan]

Yeah the statement is broken on many levels :)

The NS problem is effectively: decide if the proof of MillenniumProblemStatement is by Or.inr or Or.inl :) (assuming that two options are formulated correctly)

[Ruben Van de Velde]

Timothy Chow said:

I just noticed that as far as the $10,000 bet is concerned, a crucial clause concerns uploading a paper to the arXiv in 2025. As someone who has had arXiv submissions stuck in moderation for weeks (not to mention the struggles I've sometimes had with getting an endorser for some field that I don't publish in regularly, and the stories I've heard of seemingly reasonable papers getting rejected), I wonder if the bet is going to collapse for the "silly" reason that the arXiv moderators reject the paper?

Does it say "uploading in 2025" or "being published in 2025"? /rules-lawyer

[Tomas Skrivan]

I believe that one can also prove forall p. Not (BreakdownOfSmoothSolution p) by choosing sol' : SmoothSolution with sol'.domain to be an empty set and sol'.T to be sufficiently high e.g. as sol.T + 1.

[Kevin Buzzard]

Tomas Skrivan said:

All this could result in a bad image for Lean.

I don't really think so. There are plenty of Lean repos out there that purport to do all sorts of nonsense already. The millennium prize repo isn't formally endorsed by the community and plenty of problems were pointed out with it in the other thread.

[Tomas Skrivan]

The sol'.domain = EmptySet ensures that all the conditions momentum_equation, incompressible, velocity_smooth and pressure_smoothare trivial to satisfy

[Mirek Olšák]

Oh, someone (or rather LLM?) put a default value for domain, and thought it forces that value.

[Tomas Skrivan]

Yes, that is how I see it too

[Mirek Olšák]

theorem no_breakdown (problem : MillenniumProblem) :
    ¬ BreakdownOfSmoothSolution problem := by
  unfold BreakdownOfSmoothSolution
  push_neg
  intro sol solh
  use {
    sol with
    domain := ∅
    T := sol.T+1
    T_pos := by linarith [sol.T_pos]
    momentum_equation := by simp
    incompressible := by simp
    velocity_smooth := by simp
    pressure_smooth := by simp
  }
  simp

[Mirek Olšák]

Here is my full end-to-end Lean solution of the Navier-Stokes problem on the full domain. You should forget about David Budden, and invest in my AI company, if I had one :wink: ...
MilleniumSolution.lean

[Eric Vergo]

Tomas Skrivan said:

What I'm worried about that Budden posts a proof that compiles, produces pile of reasonable/complicated looking mathematics but the AI discovers this simple hack and sneaks it somewhere in the middle. 

Given the 'physics' of reinforcement learning we should actually expect to see this sort of behavior. In fact, we already have. It’s well-known on this forum that some results have been (correctly) rescinded due to related causes.

All this could result in a bad image for Lean.

My opinion is that this was handled by the community here pretty well. That should matter for any one who is paying attention. I think @Weiyi Wang  was correct in saying that there had not been any topics on this up until now. Please correct me if I’m wrong. I’m guessing that everyone here had mostly the same reaction : “show me the files or there is nothing to talk about”.

Then when files were shared people, including some here, responded on twitter showing the obvious flaws and that was that. My understanding is that some of the surrounding discourse was not great. But, I’d rather not discuss specifics because I don’t want to bring any discourse of that sort to the forum. This really is a pleasant place and we should keep it that way. It's also very easy to find, so you can inform yourself if you wish.

Not sure what to do about it though.

We have ‘the first sketch’ of something here: #general > TAIL - Template for AI generated Lean proofs @. It is far from perfect and as @Jason Rute noted there are many flaws. More importantly there are multiple healthy discussions going on covering various aspects of 'soundness’ beyond bugs. Along with those discussions are tools being built to check for the soundness issues (Lean4Checker, Comparator, lean4lean, SafeVerify, etc.). Maybe this should get a dedicated channel? 

My opinion is that even if all the tools being discussed are executed on well and adopted, it won’t be a panacea. The evidence suggests that we will still be faced with volume problems.

[edit: removed a misquote]
[second edit: it seems there was some public, albeit ad-hoc discussion of the claim before I made this post. ]

[Artie Khovanov]

re community members with influence / credibility engaging with this: one option is to brief journalists off the record, and explain the reality of such situations to them bluntly
that way there is pushback to the media on dubious / crank / viral social media claims, but nobody needs to violate academic norms (which are unfortunately ill-suited to the contemporary media environment)

[Eric Vergo]

Mirek Olšák said:

theorem no_breakdown (problem : MillenniumProblem) :
    ¬ BreakdownOfSmoothSolution problem := by
  unfold BreakdownOfSmoothSolution
  push_neg
  intro sol solh
  use {
    sol with
    domain := ∅
    T := sol.T+1
    T_pos := by linarith [sol.T_pos]
    momentum_equation := by simp
    incompressible := by simp
    velocity_smooth := by simp
    pressure_smooth := by simp
  }
  simp

Man simp is completely over-powered. If we are really going to claim that "Lean is the best video game in the world" I think we should consider nerfing for metagame reasons.

[Mirek Olšák]

simp is the high-tech AI that solved a millenium prize problem!

[Timothy Chow]

Ruben Van de Velde said:

Does it say "uploading in 2025" or "being published in 2025"? /rules-lawyer

"DB bets that he will upload a paper to arXiv.org during the calendar year 2025 that provides a solution to the Navier-Stokes Smoothness and Existence problem."

If he initiates his upload in 2025 and it is accepted and published in 2026 then I don't see any issues. But if his paper is rejected then I'm not sure what that means. Does an attempted upload still count as an upload if the attempt fails?

[Mirek Olšák]

The bet requires

• Budden submitting a proof to arXiv
• Clay Mathematics Institute recognizing that paper as a solution to Navier Stokes

That doesn't exactly require the paper to be accepted to arXiv. It could in theory happen (and count as Budden winning the bet) that Budden submits a solution to arXiv, the solution is rejected, but later he publishes the same solution by other means, and gets recognized by Clay Mathematics Institute.

[Timothy Chow]

Mirek Olšák said:

The bet requires

• Budden submitting a proof to arXiv

The bet uses the word "upload" and not the word "submit." Your interpretation seems reasonable, but I'd argue that it's also reasonable to say that if a paper does not appear on the arXiv then it hasn't been uploaded to the arXiv.

[Kevin Buzzard]

I think that discussions about whether a non-existing arxiv paper satisfies the conditions of a bet are probably off-topic here. There is no lean code so there is no story as far as this forum goes.

[Eric Wieser]

Yaël Dillies said:

Does rintro ⟨sol, ⟨⟩⟩ also work?

Or better, nofun

[Eric Wieser]

I'll push these golfs to https://github.com/eric-wieser/navier-stokes-misformalization, let me know @Mirek Olšák if you'd prefer me to transfer the repo to you

[Mirek Olšák]

No strong preferences, I did it mostly for fun -- if Budden can brag about a Lean solution of Navier Stokes, we can do the same but better. That is why in the original file, I didn't explicitly say it was not a real solution (although it should be obvious to any sane person).

When it is published in a repo, maybe it will be worth it to explain there which mistakes it exploits (I can do later, I accepted the github invitation).

[Jason Rute]

I just want to point out that the Lean code Budden has posted (at least one screen shot, 2 files on separate occasions, and a file he shared privately with Elliot Glazer---but tweeted about sharing) tell a fairly simple story. At first, his files were very circular in their logic with lots of axioms and assumptions but which also didn't compile. After coaching from Elliot, it seems Budden has learned how to use Lean correctly. His only Lean file which typechecks is also quite incomplete (and I think it uses the sup norm when he meant to use the L2 norm FWIW). It is not a complete proof of NS by any means. And finally he posted a screen shot showing the many errors he is still trying to fix, which is the last we heard of him.

[Jason Rute]

I know there is a lot of worry that his "proof" is using Lean exploits, but it really seems that he has never had anything remotely resembling a working Lean proof, and any public claims to that effect on Budden's part have been ambitious promises to deliver, not based on him having a "working" Lean proof up his sleeve. (I'm mostly getting this by him saying things about writing all the code at the last minute, implying that he never had full Lean proof. And also that none of his code seems to be very complicated.)

[Jason Rute]

I'm personally not worried about exploits for a Lean millennium problem proof. This community would quickly scrutinize a Lean millennium problem solution, and be able to reduce it to either interesting non-trivial mathematics or to trivial broken Lean. We have many tools for inspecting proofs and guarding against exploits and we would come up with many more if a Millennium problems was involved. (And no journal or prize committee would be quick to announce a resolution until the Lean community was happy with the Lean proof.) I worry a lot more about the little theorems that aren't going to get the attention of a Millennium problem (which is why I keep harping about coming up principled and complete standards of correctness for Lean proofs).

[Jason Rute]

Kevin, I hope I'm staying on topic here.

[Jason Rute]

Also, if as stated above, the statement of NS is wrong in Lean Dojo, then I think it is important to do the following two things.

1. Make an issue or PR on the Lean Dojo github (and maybe also for the other Millennium problems) highlighting the error. Considering how important these problems are and how official this repo looks, I think it is important to make it clear this is not a correct formalization. I assume @Anima Anandkumar and @Robert Joseph would be happy to correct the issue. (Also, @Elliot Glazer you should know, since you are one pushing for using this formalization.)
2. Ideally one should make a correct NS statement somewhere more official, namely in Mathlib or the Formal Conjecture project. (This isn't my field, so I don't know how hard it is to correctly formalize NS.)

[Timothy Chow]

Jason Rute said:

I worry a lot more about the little theorems that aren't going to get the attention of a Millennium problem (which is why I keep harping about coming up principled and complete standards of correctness for Lean proofs).

The question, I think, is whether the publicity associated with a Millennium problem can be a helpful catalyst for coming up with such standards.

The bet with Budden is potentially on-topic, because jacking up the bet to $1 million provides a potential source of funding for such an effort. If Budden is willing to raise the stakes, and is serious about paying up when he loses (in exchange for the publicity and Lean support that he'll get), then I think I can probably find someone to escrow the money for the other side of the bet (assuming, say, the CMI is willing to act as the independent third party).

Unfortunately, the more I read, the less confident I am that Budden has $1 million to spare. If someone close to him knows otherwise, then I'm happy to talk more offline.

[Mirek Olšák]

Jason Rute said:

Also, if as stated above, the statement of NS is wrong in Lean Dojo, then I think it is important to do the following two things.

1. Make an issue or PR on the Lean Dojo github (and maybe also for the other Millennium problems) highlighting the error. Considering how important these problems are and how official this repo looks, I think it is important to make it clear this is not a correct formalization. I assume Anima Anandkumar and Robert Joseph would be happy to correct the issue. (Also, Elliot Glazer you should know, since you are one pushing for using this formalization.)
2. Ideally one should make a correct NS statement somewhere more official, namely in Mathlib or the Formal Conjecture project. (This isn't my field, so I don't know how hard it is to correctly formalize NS.)

As discussed with @Tomas Skrivan here, the issues with the formalization are more profound. Rather than "We found this little bug, fix it, and it should be fine", the status is "We didn't even look into the deep math yet, and already found three flaws, so we are afraid that the whole formalization needs to be rewritten with experts." If there are indeed (as you suggest) people willing to spend their time on formalizing & checking the formalization of Navier Stokes, then great. Otherwise, I am not sure exactly what the github issue should say besides "Navier Stokes is wrong, here is an example how we can make the current version trivial, more work & examination needs to be done."

[Eric Wieser]

I think opening that issue as described with a link to this thread (and/or my repo) is valuable

[Yaël Dillies]

Jason Rute said:

Ideally one should make a correct NS statement somewhere more official, namely in Mathlib or the Formal Conjecture project.

The quick way to increase the likelihood of this happening would be to open an issue on the formal-conjectures repo: https://github.com/google-deepmind/formal-conjectures/issues

[Yaël Dillies]

There are currently a handful of contributors (mostly students in Indian universities, it looks like?) who are roaming the issues looking for something nice to state formally, and right now I review their PRs rather quickly. If Navier-Stokes is made into an issue, I'm sure someone will take it on within a few weeks.

[Elliot Glazer]

Jason Rute said:

1. (Also, @Elliot Glazer you should know, since you are one pushing for using this formalization.)

Good to know! I did specifically say on Twitter that I didn't consider the LeanDojo formalizations to be sufficiently scrutinized and that I was hoping for the mathlib community to get more involved with conjecture formalization. I'll make a post that there is in fact substantial skepticism about the NS formalization.

Speaking of lists of formalized conjectures, how much scrutiny has DeepMind's repo gotten?

[Yaël Dillies]

Many AI companies use it as a benchmark for their maths LLMs, as well as professional and amateur mathematicians (such as Boris Alexeev) as a way to formalise their progress on Erdos problems. Therefore it is expected that most of the simple misformalisations are found quickly (but not necessarily solved quickly, as AI companies have potentially an incentive to keep fixes secret).

[Mirek Olšák]

https://github.com/lean-dojo/LeanMillenniumPrizeProblems/issues/4

[Yaël Dillies]

Furthermore, contributions are reviewed by Lean experts (mostly Moritz Firsching and I right now, but also Paul Lezeau and Calle Sönne previously). This doesn't mean the statements are absolutely correct, however. I have myself merged wrong statements just last week.

[Elliot Glazer]

I find it quite irresponsible that the LeanDojo team gave one of their own NS formulations a 5/5 completeness rating, given the insufficient scrutiny. I think non-mathlib project maintainers should show substantial epistemic humility about their projects' accuracy.

[Jason Rute]

As for DeepMind’s FormalConjectures repo, I think everyone is aware that it is REALLY hard to state problems without errors, so I think there are likely lots of mistakes, and some have already been found. But at the same time, I’ve felt the team making that repo has show a lot of professionalism.

[Tomas Skrivan]

Should I make a PR to formal-conjecres?

import Mathlib

open ContDiff Set InnerProductSpace MeasureTheory

local macro "ℝ³"  : term => `(EuclideanSpace ℝ (Fin 3))

structure InitialVelocityCondition (v₀ : ℝ³ → ℝ³) : Prop where
  smooth : ContDiff ℝ ∞ v₀
  decay : ∀ n : ℕ, ∀ K > 0, ∃ C : ℝ, ∀ x, ‖iteratedFDeriv ℝ n v₀ x‖ ≤ C / (1 + ‖x‖)^K

structure ForceCondition (f : ℝ³ → ℝ → ℝ³) : Prop where
  smooth : ContDiffOn ℝ ∞ (↿f) (Set.univ ×ˢ Set.Ici 0)
  decay : ∀ n : ℕ, ∀ K > 0, ∃ C : ℝ, ∀ x, ∀ t ≥ 0, ‖iteratedFDeriv ℝ n (f · t) x‖ ≤ C / (1 + ‖x‖ + t)^K

noncomputable
def div (v : ℝ³ → ℝ³) (x : ℝ³) : ℝ := (fderiv ℝ v x).trace ℝ ℝ³

structure NavierStokesExistenceAndSmoothness
    (rho nu : ℝ) (v₀ : ℝ³ → ℝ³) (f : ℝ³ → ℝ → ℝ³)
    (v :  ℝ³ → ℝ → ℝ³) (p : ℝ³ → ℝ → ℝ) : Prop where

  navierStokes : ∀ x, ∀ t > 0,
    deriv (v x ·) t + fderiv ℝ (v · t) x (v x t) = - rho⁻¹ • gradient (p · t) x + nu • Δ (v · t) x + f x t
    ∧
    div (v · t) x = 0

  initialCondition : ∀ x, v x 0 = v₀ x

  velocitySmoothness : ContDiffOn ℝ ∞ (↿v) (Set.univ ×ˢ Set.Ici 0)
  pressureSmoothness : ContDiffOn ℝ ∞ (↿p) (Set.univ ×ˢ Set.Ici 0)

  integrable : ∀ t ≥ 0, Integrable (‖v · t‖^2)
  globallyBoundedEnergy : ∃ E, ∀ t ≥ 0, (∫ x : ℝ³, ‖v x t‖^2) < E

theorem navier_stokes_existence_and_smoothness
  (rho nu : ℝ) (v₀ : ℝ³ → ℝ³)
  (hrho : rho > 0) (hnu : nu > 0) (hv₀ : InitialVelocityCondition v₀) :
  ∃ v p, NavierStokesExistenceAndSmoothness rho nu v₀ (f:=0) v p := sorry

theorem navier_stokes_breakdown (rho nu : ℝ) (hrho : rho > 0) (hnu : nu > 0) :
  ∃ (v₀ : ℝ³ → ℝ³) (f : ℝ³ → ℝ → ℝ³),
    InitialVelocityCondition v₀ → ForceCondition f →
    ¬(∃ v p, NavierStokesExistenceAndSmoothness rho nu v₀ f v p) := sorry

[Yaël Dillies]

Please do!! Can't promise I will merge it quickly though. This one might take a while to review.

[Tomas Skrivan]

I do not know how to formulate that you should prove either navier_stokes_existence_and_smoothness or navier_stokes_breakdown as Mirek pointed out the naive way would be effectivelly P ∨ ¬P.

[Mirek Olšák]

Making it two conjectures is reasonable.

[Mirek Olšák]

Is it easily provable that one is a negation of the other?

[Tomas Skrivan]

There are two things I'm unsure about

• should it be t > 0 or t ≥ 0 in NavierStokesExistenceAndSmoothness.navierStokes
• the ‖iteratedFDeriv ℝ n v₀ x‖ is not exactly the same as wiki's |∂^α v(x,t)| I don't really know how is the norm on multilinear maps is defined but as it is on ℝ³ so it should be equivalent. But it is not word by word.

[Tomas Skrivan]

Mirek Olšák said:

Is it easily provable that one is a negation of the other?

I don't think so as the positive result assumes that the force term f is zero for some reason.

[Yaël Dillies]

Tomas Skrivan said:

I do not know how to formulate that you should prove either navier_stokes_existence_and_smoothness or navier_stokes_breakdown

The style in FC is to write answer(sorry) \iff ... and let the LLM replace sorry by either True or False

[Mirek Olšák]

Oh really? I thought that it is implicit about conjectures that you are supposed to prove or disprove them.

[Tomas Skrivan]

Yaël Dillies said:

Tomas Skrivan said:

I do not know how to formulate that you should prove either navier_stokes_existence_and_smoothness or navier_stokes_breakdown

The style in FC is to write answer(sorry) \iff ... and let the LLM replace sorry by either True or False

I'm not following, what LLM?

[Tomas Skrivan]

Mirek Olšák said:

Oh really? I thought that it is implicit about conjectures that you are supposed to prove or disprove them.

Yeah I find it confusing too, maybe the version with non-zero force can be easily reduced to the case with zero force.

[Mirek Olšák]

So it is at least easy to see that both options do not hold at the same time?

[Yaël Dillies]

Tomas Skrivan said:

I'm not following, what LLM?

I mean whichever LLM whoever uses when they are trying to solve Navier-Stokes automatically.

[Tomas Skrivan]

Ohh I see, so I should write

theorem ... : answer(sorry) ↔ P  := sorry
theorem ... : answer(sorry) ↔ ¬P  := sorry

where P is the conjecture?

[Mirek Olšák]

Mirek Olšák said:

Oh really? I thought that it is implicit about conjectures that you are supposed to prove or disprove them.

This was a reaction to Yael's comment about answer. In olympiad problems, we distinguish between "prove that X", and "decide if X", but this distinction doesn't make sense for open problems.

[Mirek Olšák]

Do you do this now with every open conjecture?

[Tomas Skrivan]

Mirek Olšák said:

So it is at least easy to see that both options do not hold at the same time?

Surprisingly, I'm not sure :) At first sight you might have a solution for every initial condition when force is zero but there might be a breakdown when force is non-zero.

I should also check the formulation by the Clay Institute.

[Eric Wieser]

Mirek Olšák said:

Oh really? I thought that it is implicit about conjectures that you are supposed to prove or disprove them.

For conjectures of the form "P is true", we write theorem ... : P. For open questions of the form "Is P true?" we write theorem ... : answer(sorry) ↔ P.

[Timothy Chow]

I'm not sure this matters for the current discussion, but for 4 of the 6 remaining Millennium Prizes, the CMI promises the award only if you prove the conjecture, not necessarily if you disprove it. Though Navier-Stokes is one of the two (along with P = NP) that come with a prize whichever way you resolve it.

[Eric Wieser]

Tomas Skrivan said:

I should also check the formulation by the Clay Institute.

The wording includes "To give reasonable leeway to solvers while retaining the heart of the problem, we ask for a proof of one of the following four statements.", so it would be appropriate to write the four separately in addition to the general statement

[Yaël Dillies]

Tomas Skrivan said:

Ohh I see, so I should write

theorem ... : answer(sorry) ↔ P  := sorry
theorem ... : answer(sorry) ↔ ¬P  := sorry

where P is the conjecture?

Only one is enough

[Tomas Skrivan]

The trouble is that it is not exactly P and Not P

[Tomas Skrivan]

I will just write down all four statements separately, exactly as stated in the official formulation and as Eric suggests

[Eric Wieser]

For formal-conjectures, it's also valuable to write down the known results that the document mentions

[Tomas Skrivan]

I will leave that to someone else :)

[Eric Wieser]

It's highly likely that an AI system will be able to reproduce those long before making headway on the real problem, and in doing so it is likely to flag misformalizations

[Eric Wieser]

(I mean write down their statements not their proofs!)

[Mirek Olšák]

Then my understanding is that these A, B, C, D are 4 conjectures (although sometimes contradictory to with each other), not questions. So they should be written individually without answer(sorry).

[Tomas Skrivan]

Hmm the partial result is an order of magnitude harder and might require Sobolev spaces that we do not have in mathlib yet. I definitely do not feel confident enough to formulate it.

[Tomas Skrivan]

Mirek Olšák said:

Then my understanding is that these A, B, C, D are 4 conjectures (although sometimes contradictory to with each other), not questions. So they should be written individually without answer(sorry).

I agree, as resolving it as False <-> ... is not what the official statement require

[Tomas Skrivan]

The PR is ready: https://github.com/google-deepmind/formal-conjectures/pull/1457

[Eric Vergo]

Jason Rute said:

As for DeepMind’s FormalConjectures repo, I think everyone is aware that it is REALLY hard to state problems without errors, so I think there are likely lots of mistakes, and some have already been found.  But at the same time, I’ve felt the team making that repo has show a lot of professionalism.

There is an important meta point here. We are in a position where:

1. People are generally acting in good faith

2. We're operating in a high-rigor domain with substantial scrutiny around certain results

3. Things still slip through the cracks

Indeed, this is because what we are doing is very hard, but it's still happening.

Jason Rute said:

We have many tools for inspecting proofs and guarding against exploits and we would come up with many more if a Millennium problems was involved.   (And no journal or prize committee would be quick to announce a resolution until the Lean community was happy with the Lean proof.)  I worry a lot more about the little theorems that aren't going to get the attention of a Millennium problem (which is why I keep harping about coming up principled and complete standards of correctness for Lean proofs).

I would much prefer we take a proactive stance rather than a reactive one. Not because of the millennium problems, or even the smaller ones as you mention. I do share those concerns but am more motivated by the following point: the stakes surrounding claims of proofs in Lean have increased substantially. This community has suddenly, and somewhat unexpectedly, found itself close to the center of a technology with significant downstream consequences. Here is what I mean:

For many years, proving mathematical statements in Lean was low stakes in the sense that few, if any, people outside of the math/Lean community cared if there was a mistake in a formalization of a mathematical proof. Yes, people used Lean to engineer and ensure safety aspects of critical systems, but that's not what I'm talking about. That was and still is important in the way that I am suggesting.

What has changed is the importance of things like proofs of IMO problems. A few years ago if we mis-formalized some random problem or validated a proof that hid the exploitation of some bug, it really didn't matter as there were no externalities. Now, all of a sudden, this is not the case. People are using Lean to evaluate (and more importantly, increase) the capability of their LLMs. Then, they are using those LLMs to attempt things like accelerate the rate of discovery in science, capture trillions of dollars in value via automating labor, and pursue other high-impact goals. What we are doing here matters for the rest of the world, even if most people are completely unaware that we exist.

What concerns me most is the speed at which all of this is happening. A year ago, o1 had just been released as the first "thinking" model, and it was fairly inept at writing proofs in Lean. Now things like this are happening. How good will they be this time next year? What about six months from now?

Consider what things will look like for us if the models do get substantially better in a relatively short period of time. Does anyone here feel like we would be ready for that? I certainly don't.

[Jason Rute]

I do agree with being proactive but I also worry about overreacting. For example, I saw someone get very worried on X about Budden’s first Lean code using native_decide. But in the big picture, native_decide isn’t a large issue. Yes, it is inconsistent in theory, but it has practical uses and sometimes works as a first step. (And Budden’s code didnt even compile at that point.) I’ve also seen some possible overreactions about Lean’s kernel having a few small soundness bug found in the last year.

[Mirek Olšák]

I would remark that my issue with native_decide was not that it was present but that it was allegedly used to prove

  have h_exp : Real.exp (-2) < 0.14 := by native_decide

which is not in the competence of native_decide (unless you refactor real numbers).

[Elliot Glazer]

Jason Rute said:

I do agree with being proactive but I also worry about overreacting. For example, I saw someone get very worried on X about Budden’s first Lean code using native_decide. But in the big picture, native_decide isn’t a large issue. Yes, it is inconsistent in theory, but it has practical uses and sometimes works as a first step. (And Budden’s code didnt even compile at that point.) I’ve also seen some possible overreactions about Lean’s kernel having a few small soundness bug found in the last year.

I think if someone wants to claim "I have proven a super famous conjecture and I did it in Lean," there is a massive onus on them to do so to the highest standards. So even though native_decide is a yellow flag rather than a red flag, I don't feel it's unwarranted to criticize it being used in this context.

[Snir Broshi]

FWIW

import Mathlib
example : Real.exp (-2) < 0.14 := by
  rw [show (-2 : ℝ) = (2 : ℕ) * -1 by norm_num, Real.exp_nat_mul]
  grw [Real.exp_neg_one_lt_d9]
  norm_num

[Eric Wieser]

It looks like Budden has decided that Lean makes it too hard to get away with writing nonsense

Lean can seriously go [expletive].
(I endeavour to finalise this, but I tell you what. I'm fighting an uphill battle with mathlib, not with LLMs)

[Mirek Olšák]

Easy to make fun... but it is true that Lean is far from the convenience of algebra systems for differential equations. I would only expect that a system so smart that it can solve a millennium problem could tackle this somehow too.

[Jason Rute]

One of Budden’s main complaints was that his local version and the web version, even though they are both 4.X.Y, are not compatable. Given the way Budden is behaving I don’t think anyone would be willing to help him with this. Elliot was encouraging Budden to make his code compatible with the web editor so that it was easy for others to check. Budden was never open about how he was using Lean, including how he installed it, if he was using Lake, and when version he is on locally. If he posted full git repos with a lake file instead of just single files it would have helped a lot.

[Eric Wieser]

It wasn't clear to me whether Budden was saying that he had 4.X.Y in both places and they were incompatible, or that 4.X1.Y1 was not compatible with 4.X2.Y2 despite semver versioning (which AIUI Lean does not explicitly claim to use) saying they should be compatible..

[Eric Wieser]

Though based on the errors he was getting from the WithLp refactor which landed more than a release ago, I think it was the latter

[Jason Rute]

Oh, I thought it was the latter, but the former would be weirder (but not surprising given all this).

[Eric Wieser]

The former would come down to "ah, but 4.X.Y is the lean version, and you're using the bleeding edge of mathlib"

[Eric Wieser]

@Henrik Böving, here's a feature request that might help with this; could hovering over import Mathlib.Foo include some hover text that summarizes the lake-manifest.json?

[Henrik Böving]

Meta question: Why are you asking me? :sweat_smile:

[Eric Wieser]

Whoops, I meant @Marc Huisinga !

[Marc Huisinga]

I don't think that displaying this kind of information on every import hover is the right place for it (it's a lot of information, so a pretty large hover, and I wouldn't expect to find it there). We could have a VS Code command (under 'Project Actions' in the forall menu) that displays information from the manifest in a nicer form, though (or something similar).
In either case, I also think that this kind of feature wouldn't have helped prevent the Budden situation.

If you feel that this is important, could you write a vscode-lean4 RFC for this @Eric Wieser?

[Eric Wieser]

To be clear, the suggestion is to only display information about the source of Mathlib (the relevant import), not every item in the manifest. In most cases this could simply be a single sentence with a link to GitHub or reservoir

[Marc Huisinga]

Doing this in the language server is pretty complicated. Since I also feel that attaching this kind of information to an import hover is not very discoverable, I'd much prefer a VS Code command for the whole project.