NYTimes.com: A.I. Can Now Write Its Own Computer Code. That’s Good News for Humans.

[John Clark]

From The New York Times:

A.I. Can Now Write Its Own Computer Code. That’s Good News for Humans.

A new technology called Codex generates programs in 12 coding languages and even translates between them. But it is not a threat to professional programmers.

https://www.nytimes.com/2021/09/09/technology/codex-artificial-intelligence-coding.html?smid=em-share

[Lawrence Crowell]

I am learning about Coq, which is a theorem proving/proof checking system. The one problem with this or some AI code generating system is that we humans will start losing more contact with how things actually work.

LC

[Brent Meeker]

That's interesting.  Does Coq let you change axioms?  In what Feynman called "Persian" mathematics, you're interested in what axioms support a given theorem, not the other way around as in "Greek" mathematics.

My wife (who's a mechanical engineer) were just discussing how calculus is regarded as the "hard mathematics" in college.  But I wonder if it's a matter of how it's taught.  When she and I went school a lot of calculus was learning tricks and approximations to do integration.  Conceptually it wasn't that hard.  And in applications, nobody worries much about the tricks anymore because they just give it a computer.  Mathematica knows the tricks and there's easy numerical integration algorithms.  Does that mean we are losing contact with how it actually works...not at all.  Those tricks and approximations just obfuscated "what was really going on".

I wonder how calculus is taught now in high school and undergrad college courses?  ISTM is could be much clearer and conceptual and easier to learn.

Brent

--
You received this message because you are subscribed to the Google Groups "Everything List" group.
To unsubscribe from this group and stop receiving emails from it, send an email to everything-li...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/everything-list/453c2c88-fcf0-4fac-9129-7798ad3b8f07n%40googlegroups.com.

[Lawrence Crowell]

It is sort of like that. You can propose any axiomatic system you want.

 Matiyasevich proved that Hilbert's 10th problem was unsolvable. This 10th problem was to find a universal method for solving Diophantine equations. This turns out to to mean there is no axiomatic system for solving p-adic number systems. There are then an infinite number of such number systems. You can build them almost as you want.

LC