vilhelm_s

My point is that Astra did not write the statement of Navier-Stokes in Lean, there was already a human-written statement, so there should be no concern that it has errors.

This article shows that we can't conclude from the working Lean proof that the NL proof is also correct, because they are different in some places. On the other hand I think it's unlikely that it's "very" broken. OpenAI first spent a lot of computer time to find the NL proof, and then less time to translate it into Lean. So if there were errors in the NL proof it seems they were not fatal, the agent translating it into Lean was able to patch them up as it went along.

The "statements" here are statements of lemmas, not the statement of the main theorem. The main theorem statement was written by humans (prior to the OpenAI work), so there shouldn't be any concern that an AI mistranslated it.

The OpenAI announcement says

> 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.

This seems pretty clear that they found the proof first and then mechanized it afterwards.

The "shall" in the standard means it's undefined behavior. This is explained in the "Conformance" section,

> 2. If a ‘‘shall’’ or ‘‘shall not’’requirement that appears outside of a constraint is violated, the behavior is undefined. Undefined behavior is otherwise indicated in this International Standard by the words ‘‘undefined behavior’’ or by the omission of any explicit definition of behavior. There is no difference in emphasis among these three; they all describe ‘‘behavior that is undefined’’.

Compilers will not refuse to compile the code, indeed the blog post we are all commenting on reports the results from a bunch of different compilers. Historically the reason the C standard specified a lot of undefined behavior is that the actually existing C compilers at the time compiled the code but disagreed about the output.

Yeah. I guess the abstract type approach saves some memory, but it's a constant factor thing, not an asymptotic improvement. The comment that Lean wastes "tens of megabytes" seems telling: it seems like something that would be a critical advantage in the 1980s and 1990s, when Paulson first fought these battles, but maybe less important today...

The order was not that he had to produce the coins, just that he cooperate in tracking them down. Telling them where he had stashed it would have been fine.

We need to do "leap hours" anyway--just today they changed to daylight saving time in the U.S.! And time zones are also adjusted every now and then, which also amounts to a one-hour change in the affected regions. Even if we didn't have continous practice with leap seconds, I think we could definitely include an extra one-hour shift for earth rotation reasons along with all the other ones.

I don't think it's that subtle: it would be enough to have a continuous integration tool that tries to compile the proofs that are checked into version control and raises an error if it fails.

The linked blog post says "Unfortunately, a student once submitted work containing this error; it was almost entirely incorrect and he had no idea." I guess the student probably was aware that not every proof had gone through, and that the that he saw like "99 out of 100 proofs succeeded" and assumed that meant that he had mostly completed the task, not realizing that a false theorem would be used to the give incorrect proofs for the rest of the file.

The idea is that e.g. the government would give you an app that lives on your phone. When you apply for the app you provide some documents to prove your age, but you don't say anything about what sites you plan to visit. When you want to visit an age-restricted site you use the app to generate a proof that you have it, but the site doesn't learn anything more than that, and the government doesn't learn that you used the app.

Yeah, that sounds very unlikely. The full paper dismisses the possibility:

> Another possible explanation to consider is that the current indings were caused by cross-cueing (one hemisphere informing the other hemisphere with behavioural tricks, such as touching the left hand with the right hand). We deem this explanation implausible for four reasons. First, cross-cueing is thought to only allow the transfer of one bit of information (Baynes et al., 1995). Yet, both patients could localize stimuli throughout the entire visual field irrespective of response mode (Experiments 1 and 5), and localizing a stimulus requires more than one bit of information. Second, [...]

I get the impression that the authors of the paper have some kind of woo (nonmaterialist) view of consciousness. But they also mention this possiblity, which seems more plausible to me:

> Finally, a possibility is that we observed the current results because we tested these patients well after their surgical removal of the corpus callosum (Patient DDC and Patient DDV were operated on at ages 19 and 22 years, and were tested 10–16 and 17–23 years after the operation, respectively). This would raise the interesting possibility that the original split brain phenomenon is transient, and that patients somehow develop mechanisms or even structural connections to re-integrate information across the hemispheres, particularly when operated at early adulthood.

They are regulating websites anyway, surely they can just invent some standard format to say what function each cookie has. How about requiring that the name of every cookie has to start with one of "Strictly Necessary", "Functional", "Performance", and "Targeting/Advertising"?