I'm not sure what enterprise-level collaboration means. In my experience, "enterprise" usually means: "Let's use tools that are 10 years behind, buggier than average, and have lots of half-baked features, none of which we need".
I'm not sure what kind of tools you mean, but unless you're looking for something that just works exactly the way EJBs do for some mysterious reasons, I don't see why you can't do most "enterprisey" things with Rust or Go. Or Python or TypeScript for that matter.
Yes and that's exactly what modern tooling is missing. Try to develop for node.js 0.2.12 on today's update of Visual Studio Code. See? No enterprise-level collaboration for ya.
Probably something about integrating access control to a repository so a deparment has the source for a certain library, while the others only see the header files and compiled objects to use?
I have found these models to be useful either at super specific tasks (e.g., "take this function or algorith?m and find any black magic to make ot faster + validate and verify the hell oit of it"), or give it an entire thing to oneshot without oversight. The moment you have a hybrid workflow where you actually have to work and check and understand AI code, things get insane
There are also plenty of things a compiler might not expose that end up being ambiguous. For example, C++ doesn't officially have a restrict keyword, so how can you express the fact that two memory regions never operlap and can be optimized? Unfortunately the reality is that if we had a language capable of truly expressing the programmer's intent we'd end up with a monster
>For the past year, Buckmaster and Alpöge had been using a variety of AI tools, including OpenAI’s Codex, to tackle the Navier-Stokes problem. Last month, their AIs had at long last found a solution to the Euler equations and verified it in Lean.
The surface of bugs in Lean is infinitely smaller than the human error involeved in a committee of peer reviewers. It's way more probable to say "it's proven because Lean says so" than "it's proven because a couple of reviewers said so".
Also, if a bug is found, all previosuly proven theorems can be reproven to immediately and conclusively find out if things went wrong somewhere
Godel proved that any system expressive enough to produce an arithmetic is incomplete. He initially proved it for the peano axioms but then it got generalized. ZFC can produce an arithmetic. Also, before being arrogant and demanding explanations, you should give them first for your claims
you understand that "expressive enough to produce" are not obvious elements of zfc, that's some average consumer napkin math and not strict formalization.
That increases the likelihood that they are right.
> support your point with explanation or be ignored :-)
Anyone who says "Godel theorems are for systems with basic arithmetic, zfc doesn't include arithmetic, thus are not object of Godel theorems" and isn't joking warrants a permanent ignore.
A quick google search shows different proof assistants have been used to obtain the Peano axioms from ZFC, such as Isabelle/ZF and Metamath. I think you're just wrong
coming back to your argument about peano being obtained from zfc, you obviously can't prove that it happened using purely zfc, and not some logical framework embedded into those proof assistants.
I said I am not expert, I am indeed not expert in zfc and godel theorems, but I am an expert (phd) in actual formalization theory.
Formal theory is very simple concept: its alphabet, set of formulas on top of this alphabet, and function which translates one formula to another.
ZFC can't "obtain" peano, simply because it doesn't have say * operator defined. You need to do something on top of it.
Additionally, zfc itself looks like loosely formalized say in wikipedia (and I am not sure if there is any strict formalization anywhere), we take it as common sense that it can utilize some simple logical rules (e.g. modus ponens), but what are exactly rules, which could be separate topic of research, this detail is skipped.
Eh? Any first course in set theory will present ZFC as a one-sorted theory with ten axioms (/schemas) in first order logic (inheriting an equality symbol, forall, implies etc) with one binary predicate (namely set membership), or will present a theory that is equiconsistent with a usual ZFC presentation. Honestly I’m not sure how you simultaneously claim to be a PhD in formalisation and also not be aware of the existence of Isabelle/ZF, for example.
I referred to specific definition in wikipedia.
Your "first course notes" are irrelevant here, they can't be reviewed, they not proofread and unlikely can be considered as any reasonable quality if we are talking about real formalization of math.
reply