latent-person
Joined 3 months ago
Karma
63
Submissions
28
Member since
Jul 22
Recent submissions
Comment · 10 days ago
https://en.wikipedia.org/wiki/Bus_factor
Comment · 23 days ago
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.
Comment · 24 days ago
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.
Comment · 24 days ago
> 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...
Comment · 24 days ago
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).
Comment · 24 days ago
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...
Comment · 24 days ago
> 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.
Comment · 1 month ago
Yes, so basically equivalent to the code I showed in the blog.
Comment · 1 month ago
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.
Comment · 1 month ago
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...
Comment · 1 month ago
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.
Comment · 1 month ago
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?
Comment · 1 month ago
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.
Comment · 1 month ago
> 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.