numpy is pretty much all C and python. They may dispatch to some Fortran libraries, but I think basically all the internal implementations they have are C.
IIRC, scipy does (did?) actually use a lot of fortran fwiw.
I sort of wish they used c++ for some of the template stuff, especially since the code base already seems to have some C++ iirc.
I also contributed a tiny bit in the past, and their C template system was a surprise. (but this is cool and I love numpy anyway lol)
does this sort of fall into the bucket of counter-examples we've been seeing recently? I understand it's a construction causing blowup and that implies that the navier-stokes isn't regular / smooth, so sort of a counter example?
Got it. Thanks. I feel people are using this single story to downplay this feat. There's definitely a chance but I don't see any indication of similar bugs in here or the openai's proofs that were created a month ago as i think these companies might've vetted it enough and the other team who's working on similar lean proof for this also seems to have acknowledged this feat
I also doubt this is leveraging a lean4 kernel bug, but I also do not think that a 13m LoC proof that has not been human reviewed closes the book on our understanding of Fermat's Last Theorem, in part because of the decided possibility of a kernel bug being used somewhere in those 13m lines.
...I'm not saying this FLT result is compromised. I suppose things depend on your perspective where we are on the spectrum of "finding more bugs means there are fewer left to discover" vs. "finding more bugs probably means there are still unexplored corners out there".
Sure. But experts seem to be aware of the direction of those solutions so it seems unlikely there could be some hidden bug which disproves it. But it could be possible.
Well considering the proof is pretty much accepted by mathematicians to be correct (I'll be happy with that!), it would be sort of unnecessary to cheat. Maybe if some aspect is really tricky to formalize it could have done something there? If I had to search for it, I would go for parts of the original proof that are "outsourced" to other mathematical works.
Imagine one of the agents struggling to download a paper due to a paywall or whatever and just deciding to cheat lol
I think it's not unreasonable or uncommon for big O to track separate variables without reducing them, just to highlight the (lack of) sensitivity of different parameters.
I feel like at a certain point, there's is not necessarily a reason to go through the peer review publication process for some AI proofs.
Not because "ai bad," but because at some point AI outputs should probably just be treated like public knowledge. Specifically stuff that's provable by "AI please output lean showing X is true," where anyone could kind of reach the same conclusion by asking ai.
Yeah, I don't disagree with a registry. Especially for problems that are important to humans or are expensive for AI to prove/disprove.
I partly just want to avoid a situation where the volume of hard-to-search-for results that are easily-ai-proved/disproved skyrockets...
Basically, I think that for some stuff running a prompt is (or could become) easier than trying to do a search for an existing result. Partly why I think if something is fairly easily ai-proven, it should kind of be treated like it was already known, even if it wasn't actually known. :shrug:
