emileokada

If I recall correctly, they are now also only allowed to be placed where road accidents have happened before.

I thought this mathoverflow post might be of interest to those who mentioned automated theorem proving in discussions on the recent post on the ABC conjecture (https://news.ycombinator.com/item?id=18034714).

I believe the article explicitly steers away from this because nearly all the discourse on this proof has been precisely about this (c.f. remark Scholze that 'The whole discussion surrounding the proof had gotten “too sociological,”').

A lot of proofs at masters level and beyond omit a lot of details because they can easily be checked, but would be tedious to write out explicitly. This means that a 1 page proof would probably actually correspond to 2-3 pages (or more!) if written out with all the details (e.g. with standard but tedious arguments fleshed out properly, and all cases delt with explicitly (rather than resorting to a 'and the other cases follow through similarly' remark)). When written in a proof assistant this would become even longer because natural language allows us to brush a lot details under the carpet because they are understood from context.

Not convinced this is as junk as you claim it to be. From the abstract:

> While our model was solely trained with natural images, our method successfully generalized the reconstruction to artificial shapes, indicating that our model indeed reconstructs or generates images from brain activity, not simply matches to exemplars.

If I am reading that correctly it is reconstructing images that the subjects had not seen before.

It's quite staggering how many people have posted on this thread without reading the article. Nearly all the objections people have raised are directly addressed in the post.

For those who still object to the argument, would you object to me defining the piecewise function f:R->R defined to be 1/x for x =/= 0 and 0 for when x=0?

This is not true if you say division by 0 is undefined or +inf either. It really is totally fine.

> However, it is definitely possible to define some operation such that 1 `op` 0 := 0, just not the inverse operation of multiplication.

If you read the post this is actually exactly what the OP is saying.

I'm not sure what you're getting at. Classically we expect that given the same initial conditions, the outcome of a fluids experiment should always be the same. If an equation meant to describe fluid flows doesn't have this property, it is probably a bad model.

No. They've shown non-uniqueness of solutions of a strictly weaker problem. They have yet to say anything about the actual Navier-Stokes problem.