Need to know how to handle building a C++ project or dependencies? No longer have to go through dozens of posts on Reddit or DO or pages upon pages of documentation. I can just ask, then focus on what I actually want to learn.
Confused about some bizarre syntax in Haskell that gives me nothing on Google? Just ask. Don't understand how a function is constructed? Don't need to figure out what the correct terms are in what combination to find out what I'm looking at. Want a step by step explanation? Easy.
Even though it's far from perfect and I have plenty to complain about, it's already a valuable part of my everyday life with its impact on how I learn new things and experiment.
I'm not trying to be nasty, but for loops, variables, the concept of program flow etc are very elementary concepts that many children and teens are fully capable of teaching themselves, even pre-internet.
I think ChatGPT could pass any intro programming course so I have a hunch that it's just going to lead to lots of cheating and poor programming skills.
Did you end up sticking it out? Grats if so and you're probably better off for not having had ChatGPT hold your hand. For me, the temptation to just have it pass my classes for me would have been way too tempting. It's too good at boilerplate programming which is every programming 101 project.
"Write me an employee tracking system in java." Change up the comments and boom done with the assignment.
It's the same with LLMs. Now I don't have to wait hours or days for someone on SO or Reddit to read and respond to my question. Or spend who knows how long Googling for a similar - but not the SAME - question and trying to bend their solution to my problem.
And for a well trodden basic technique like mathematical induction, GPT is probably 'smart' enough to be able to explain everything.
Basically, most questions a beginner might have are already covered in something like Stack Overflow, so GPT 'just' has to give you the right cached answer, instead of coming up with new thoughts of its own. (This is very hand-wave-y.)
Induction is just set membership. Every inductive proof looks like this:
1. There's a set, S.
2. There's a scalar value, e, in S.
3. e has property p.
4. There is a function, f, from S to S.
5. f preserves property p.
6. Every element of S can be reached from e by repeated application of f. (Often because S is defined to consist of e plus f(x) for any x in S.)
---------
7. Therefore, every element of S has property p.
Terrance Tao doesn't even trust its outputs either and can verify if it is outputting nonsense that may look 'correct' in your eyes.
can you fix this? even with the (sic) I have no idea what you are trying to say here.
However, they are increasingly being used to assist human mathematicians in a variety of creative ways, beyond just brute-force case checking or computation.My impression is that most of the people who were "upset" didn't think that the result was false, or even that the work that went into the Four Color Theorem didn't constitute a proof. It's more that we mathematicians tend to like a proof more when it helps us understand why a fact is true rather than just that a fact is true. So an argument that ends with "and then we checked thousands of cases on a computer and it turned out they all worked" feels unsatisfying, since it feels like it doesn't fully explain what's going on.
> in full: sic erat scriptum, "thus was it written"
Conclusions (from slides at 49:56)
Computers by themselves still seem unlikely to resolve major mathematical problems on their own.
However, they are increasingly being used to generate (sic) assist human mathematicians in a variety of creative ways, beyond just brute-force case checking or computation.
For instance, we have seen they can be useful at generating conjectures or uncovering intriguing mathematical phenomena.
Automated provers could also be used to explore the space of proofs itself, beyond the small set of "human-generatable" proofs that often require one to stay close to other sources of intuition, such as existing literature or connections to other ways of thinking.
While AI technology shows great potential, in the immediate term, I expect it to have the most impact on tasks peripheral to mathematical research rather than central to it, such as automatically summarizing large amounts of literator or suggesting related work.
Proof formalization continues to make steady improvements in speed and ease of use. The "de Brujin factor" (the ratio between the difficulty of writing a correct formal proof and a correct informal proof) is still well above one (I estimate ~ 20), but dropping. Once AI integration takes place, this factor could potentially drop below one, which would be transformative to our field.