Earlier quoted context omitted.
the software that generated the slides is called Beamer https://en.wikipedia.org/wiki/Beamer_(LaTeX)
I believe the software was written by a German.
And people all over the world use it, not just Germans
Terence Tao: Mathematics in the Age of AI [pdf]
61–68 of 68 posts
Re: Terence Tao: Mathematics in the Age of AI [pdf]
#62Re: Terence Tao: Mathematics in the Age of AI [pdf]
#63Earlier quoted context omitted.
I believe the software was written by a German.
Vedran Miletić doesn't sound German to me! :-)
You're right, but:
- he works in Germany (https://vedran.miletic.net/files/cv-vedran-miletic.pdf)
- the original author is Till Tantau (https://www.beamer.plus/Introduction.html) who is German (https://www.tcs.uni-luebeck.de/en/mitarbeiter/tantau/cv/)
Re: Terence Tao: Mathematics in the Age of AI [pdf]
#64I think it is important to divine what currently AI is good for and what it is not even in such verifiable environments like math. Current hyped announcements about breaking conjectures are notable and are a marker of how much improvement was made. But as I read them, and maybe I am wrong, I see it as a large model+ harness executing a broad brute force search and trying solutions until something sticks. There are lo…
finally someone is saying it our loud lol. mathematicans are just finding lower and upper bounds and having a computer input them into a theorem prover more times than a human is able to on their own. ai imo isnt solving anything.
Re: Terence Tao: Mathematics in the Age of AI [pdf]
#65I 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.
You don't want people to have to rerun the prompt though. Collaborating on a registry for proven results makes sense. This probably looks like contributing Lean code to an open source project and writing docs.
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:
Re: Terence Tao: Mathematics in the Age of AI [pdf]
#66My first impressions and thoughts on the presentation speak to the need for human mathematicians to accept, absorb, and understand new AI-generated proofs—and to the fact that it takes time to do so, as well as the increasing burden of sorting through essentially unsolicited material, which robs that same group of the time to work. Software developers are seeing this same issue with AI-generated contributions of software changes in the open-source arena. What they are seeing is a very high number of trivial submissions, which Dr. Tao points out is a propensity of AI generation. The second problem is that submissions are often not good, forcing reviewers to read hundreds if not thousands of lines of intricate yet incorrect code—and they waste their productive time doing so, making them less amenable to future consideration of such contributions. This is a real problem. As to the issue of human mathematicians needing to accept work as useful before it can enter wider consideration—now that is an interesting problem if humans are indeed unable to understand work AI creates that is useful and correct, but not understood to be so (perhaps due to the above issues), and yet we have to consider a point in time when models become more capable. Let me put it another way: how long would you spend trying to get your dog to understand calculus? AI has inexhaustible patience (unlike humans), and it will keep trying to explain its ideas and theorems to us (or our dogs) far past the point humans would be willing to listen—though our dogs, at least, are amenable to treats and used to us talking a lot while handing them cookies.
Re: Terence Tao: Mathematics in the Age of AI [pdf]
#67It matters a lot what kind of tasks AI would be able to solve.
Two completely different worlds arise if AI can do what I call a modern PhD grunt work vs it being able to produce genius of Nash/Einstein/Lovelace etc.
And the way to test it is trying to produce modern math and science results with those historical LLM models or something similar:
https://news.ycombinator.com/item?id=46319826
https://news.ycombinator.com/item?id=47927903
https://news.ycombinator.com/item?id=46319826
Re: Terence Tao: Mathematics in the Age of AI [pdf]
#68Earlier quoted context omitted.
the software that generated the slides is called Beamer https://en.wikipedia.org/wiki/Beamer_(LaTeX)
I believe the software was written by a German.
sure, but the prior poster's "joke" was that Germans are bad at English and refer to overhead projectors as "beamers" when in reality the entire English-speaking academic world refers to slide decks as Beamers because they all use the Beamer software to generate their slide decks