latent-person

Correct as in the Lean proof correctly finds a counterexample to N-S.

Here is what putting trust into a Lean proof means https://ammkrn.github.io/type_checking_in_lean4/trust/trust....

In particular the main ones are:

1. The theorem has been written correctly.

2. No exploit of a kernel soundness bug in Lean (and the independent kernel nanodo, which OpenAI also checks against).

In particular, if you trust this, then you don't need to care about anything else the Lean program does, no matter how many lines, lemmas etc. it makes along the way.

As I said above, the theorem statement have been written independently by formal conjectures, and you are free to read it yourself (or trust other people have done it).

So, assuming you don't disagree the theorem statement have been written correctly, you pretty much need to believe 2 is false, if you don't trust the proof [1]. And that's what I find has a rather low probability personally.

[1] As the book says, you also need to trust the hardware, firmware etc.

In case you are not aware, the actual theorem statement of N-S was never translated by an LLM, but was written independently by formal conjectures, as they say in the README [1].

A Lean proof has a much higher probability of being correct (in my opinion) than any published (either preprint or peer-reviewed) paper, yet no one before LLMs were walking around claiming every result published can't be trusted yet (without an actual reason).

We have seen one such instance of Lean bugs, which was found adversely against Lean (as in find bug then use this bug to prove Collatz, not just found when being asked to prove it).

It's also worth to note that the way N-S (and all the other proofs by OpenAI etc) have been found is first prove it in NL then translate to Lean. I.e. it would have to first believe it found a correct proof in NL, and then afterwards either accidentally or on purpose use a Lean kernel bug.

[1]: https://github.com/openai/NavierStokesAndEuler/blob/main/Com...

edit: Probably also worth to mention that the proof have been checked both by the Lean kernel and the independent nanoda kernel, so it would need to exploit bug(s) from both.

> That's not a trivial if: stating the problem precisely is often as hard as the proof.

Really? You think 300 lines of Lean code [1] is just as hard as the proof (or even remotely close)? Also note, as the README says [2], that the theorem was written independently by formal conjectures, not by the LLM.

[1]:https://github.com/openai/NavierStokesAndEuler/blob/main/Com...

[2]: https://github.com/openai/NavierStokesAndEuler/blob/main/Com...

Or the AI wrote a NL proof of Navier-Stokes, began rewrite in Lean, then discovered a false / handwavy / easier to write in Lean / etc approach of some parts of the proof, and modified it accordingly. Since there wasn't any backpass from Lean to NL to include any changes it did due to any of the above reasons, the proofs aren't identical. That's what I think is most likely.

If the reason for the differences was done intentionally in Lean (as opposed to hallucinate e.g. m+4 vs m+5 as mentioned in remark 3.2), then a simple recording of differences, and then afterwards pass back any changes to the original NL would fix the issue. If it was hallucinated, then there is no guarantee it wouldn't keep hallucinating, and thus you might never end up with the same proof no matter how many passes you do back and forth (see remark 3.4).

Lucky that it was enough in this case. The theorem had been written by formal conjectures before the proof https://github.com/openai/NavierStokesAndEuler/blob/main/Com...

> The natural language proof was derived from the lean code, badly.

Was it? Are you claiming a LLM does reasoning in lean or what? Since this (and all the other proofs by OpenAI etc) have been in the reverse order [1]:

> The agents arrived at their resolution on Saturday, September 5, about 88 hours after the first agents were launched. Lean formalization and verification took an additional 17 hours via GPT‑6 Astra.

[1]: https://openai.com/index/navier-stokes-solution/

Yes, so basically equivalent to the code I showed in the blog.

The text right above the code says why you can't...

edit:

Let me clarify. From the blog-post:

> since a `DataFrameGroupBy` object doesn’t have a `.query()` or boolean-indexing shortcut of its own, so filtering within groups needs `.apply()` again, and the surrounding pipeline has to be rebuilt around it:

Hence you really do need one of the versions of the code I gave. You can't do the naive approach with just `.groupby().filter(lambda: )`, since you need a row-wise decision.

The problem is a small change in the question can force you to make huge changes in the code in pandas. I recently gave some examples in my blog [1]. E.g. compare the last two code blocks, where the small change is just that the median is taken within countries. This requires several line changes in pandas.

[1]https://bjarkehautop.github.io/Website/blog/data-wrangling-t...

In my opinion a better argument to stop using pandas is the very unintuitive API pandas have. Additionally, a slight change in the query can force you to restructure the whole query (change all lines), while in Polars (and tidyverse in R) it's just a simple one-line change.

Here [1] is a video made 3 months ago going over an engine vs an engine made by of one of the big YouTubers, which has 1.4m views. Enough proof?

[1]https://youtu.be/Ov7K4W-zAk0?is=6jVBkQpn8xbaA2Tz

Yes you are right, some people do watch chess engines play. TCEC (Top Chess Engine Championship) [1] streams them. Popular chess YouTubers goes over engine games from time to time too.

[1] https://tcec-chess.com/

> Lastly, let's just say that the survey source is highly suspect. It's commissioned by a British news agency with an institute whose CEO has been accused for treason and has expressed pro-succession views and has since been exiled to the UK.

Now you mistake [3] for [1] too? [3] is a peer reviewed paper (just like [2]), and neither [2] nor [3] has anything to do with Reuters (the British news agency you refer to).

Let me link [3] again for you:

[3]https://www.cambridge.org/core/journals/china-quarterly/arti...

edit:

Since max depth I'll just reply here (since you clearly also argue in bad faith). You claimed the paper had relation to a British news agency, it doesn't. So factually you are wrong, end of story.

Yes which says nothing about Reuter like you wrote 3 times?

edit:

I'll just reply here since max depth. You made a claim, that [2] has relation to Reuters. It doesn't, end of story.

This is from 1st link, not 2nd like I said?

> residents polled in a survey conducted *for Reuters* by the Hong Kong Public Opinion Research Institute

You managed to mistake [1] with [2] three times, really?

Source? And just so we are clear, are you suggesting academic malpractice, that the university intentionally designed it to be biased?

What is Reuters about the data source being a phone survey conducted by a research centre at a university in Hong Kong? (Or the 2nd source they linked to which I quoted above)?

Okay use my 2nd source then? Data source:

> The survey data reported in this article were collected via a telephone survey conducted by a research centre at a university in Hong Kong from May to June 2020.

And they also quote this paper with very similar results

> Chung, Ting-Yiu Robert, Pang, Ka-Lai Karie, Lee, Wing-Yi Winnie, and Edward, Chit-Fai, comp. 2020. Survey on Hong Kong People’s Views Regarding the Anti-Extradition Bill Movement (Round 3). Hong Kong Public Opinion Research Institute. July 10. Accessed March 19, 2025.

I summarized it with a quote? What do you want? Alternatively/also read 2nd source, which also discuss it, and again they say economic/housing was a factor, but not the largest like you claimed.

Saying a vast majority hated the protests seems like a too strong of a statement. Here are some sources which reports 57% supported [1] and 58.3% supported [2]. It has also been estimated that 36.4% had attended a demonstration against it in August 2019, and a year later 45.6% [3].

This paper directly contradicts your claim it was mainly due to housing [4].

> Our empirical findings suggested that the systematic threat concerning the erosion of the city's values and institutions imposed by the extradition bill was a primary cause of the unprecedented mobilization.

[1]https://www.investing.com/news/world-news/exclusive-hong-kon...

[2]https://www.cambridge.org/core/journals/journal-of-east-asia...

[3]https://www.cambridge.org/core/journals/china-quarterly/arti...

[4]https://www.proquest.com/docview/2714819043

(On my phone, so some sources are secondary sources).

Which has nothing to do with the total number of lines, it's just the theorem statement you need to check. Here is what they showed, which is under 300 lines with comments https://github.com/openai/NavierStokesAndEuler/blob/main/Com...

To claim something verified in Lean is wrong, you need to either argue that the theorem was stated incorrectly, or that there is a bug in Lean (assuming no `sorry` etc, which is checked by comparator). The number of lines needed to prove it is irrelevant (other than checking for a bug in Lean gets harder).

From the article:

> The finished proof was checked by Lean; it uses just Lean’s three standard axioms, and a comparator confirmed that the theorem’s statement matches Mathlib’s own statement of FLT.

So it proved the statement of FLT made independently in Mathlib. So no reason to not trust it proved the correct thing.

Not OP, but here is an example using tidyverse (I leave the meaning of it to you; should be clear without any R knowledge):

  purchases |>
    group_by(country) |>
    filter(amount <= median(amount) * 10) |>
    summarize(total = sum(amount - discount))

You should look into dplyr [1] (part of the tidyverse) in R to see how intuitive this can get. You can do math directly on columns:

  df |> dplyr::mutate(profit = Amount * Price - Losses)

For Julia, take a look at TidierData.jl [2], which provides similar tidy syntax via macros.

[1] https://dplyr.tidyverse.org/

[2] https://tidierorg.github.io/TidierData.jl/latest/

> The bare R experience is not that great

Why do you say that? Base R is arguably nicer to work with data than pandas is for example. Happy to provide specific examples to prove my point if you want.