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.

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"

A few friends of mine (who are ML practitioners!) still don't trust LLMs or find them useful in their day-to-day work.

I've noticed a similar trend among folks who work on compilers, preferring to "stay in their lane" instead of embracing GPT-4. The opposite appears true among those who work on user-facing applications, adoption of LLMs is much higher in their day-to-day.

I see a lot of people saying it's replaced some large fraction of their search usage, but they generally don't explain what type of queries they're making.

For instance, if I want to know about extreme ultraviolet lithography and I tell GPT-4 that I have a degree in engineering and that I studied advanced optics, the explanation is much richer in useful detail, going way beyond what any of the pages I could find on Google would reveal.

If you wander off of that knowledge sphere, and you are not sufficiently knowledgeable yourself about the topic, it can tell you some really stupid stuff.

Nonetheless, I do use it quite regularly in everyday life, as it is basically the best reverse dictionary (that works for any language) there is. For work (programming), I didn’t find a better use case than sometimes passing it a list of stuff, giving it an example on the first element on what I want, and using it to generate it for the rest of the elements.

But that is <1% of what I do each day.

I decided to give it another go and ask GPT-4 three questions which I needed to get answers to within the last few months.

Asking conceptually about DPO: https://chat.openai.com/share/6611454c-60de-4317-811b-2b7f31... - In this one it completely leaves out the actual trick which enables DPO, so I would say it has almost no information content. Someone who didn't know what DPO is and read this would incorrectly think that they had learned something. - To learn about this, the right place was to read the original DPO paper, and some follow-up work

Asking about FSDP compatibility with LoRA: https://chat.openai.com/share/5f8892ea-61e6-496f-abda-d5a8ad... - In this one it just says a bunch of generic vague things without answering the question. - The right place to learn the answer to this is diving through Github issue comments

Asking for details the MegaBlocks mixture-of-experts setup: https://chat.openai.com/share/c010e630-ba08-407e-afb3-03df99... - Again it's just saying generic stuff which is relevant to mixture-of-experts in general, but it leaves out everything that actually makes the MegaBlocks MoE different from a generic MoE idea - For this one I had to do a combination of reading the paper and the MegaBlocks repo

So 0/3 and pretty dramatically. I was actually expecting it to get at least one of those. As far as I can tell, it didn't really do anything different based on me specifying my background either. I'd love to see any links to productive conversations that people can share.

Now imagine they have zero problem with you interrupting them to ask the stupidest question or the most profound, difficult question, as long as you want, and if you don't like their answer you can tell them to try again. And they don't care how often you do either.

What kinds of questions might you ask that coworker in the course of your work? It's highly individual.

Then it would be able to logically reason, which it absolutely can’t do.

It’s a next generation search engine, which is very good at language-related tasks (and translating a python code it has in its training set to your language is a language task, that’s why it can be applicable to certain programming tasks).

- Copy pasted terms & conditions of a website into GPT-4 context and asked it to find the answer to a question I had.

- Copy pasted a law into GPT-4 context to check if some activity was not illegal. Hallucinations can be avoided by asking it to recite the relevant lines, then you can CTRL+F for it to double check.

- Research medical condition to point me in a vague direction

- Create shell script and desktop shortcut with custom png, to launch an application with certain parameters

- Ask perplexity.ai for the best github library for a thing I wanted to do

- Upload github library to https://app.getonboardai.com/chat and ask it questions.

- A handful of smaller things. Any error message or blocker goes straight into GPT-4.

Research into ML-guided optimisation predates chatjippity.

Almost every criticism of generative chat AI that I've seen in forums is someone holding it wrong, the direct equivalent of troubleshooting by searching for the term "my PC crashed" instead of a specific error code or whatever.

Similarly, the people complaining about ChatGPT not being very good don't realise they're using the free-tier v3.5 instead of the paid GPT4 that's much smarter. The equivalent is people who use the default browser (IE) and use the default search engine (Bing) and complain that "the Internet is not useful".

Just recently I had to review a bunch of legacy C# code, and I've found GPT4 to be enormously useful. It can find bugs and security issues in seconds, will suggest fixes to them, explain why they're bad, etc...

Note that I don't have to trust it to write security-bug-free code! I'm asking it to find bugs that I will then fix myself.

You should learn to be an effective user of LLMs, and pre-emptively use then to debug your own anti-scientific ranting and raving postings full of logical fallacies about Quantum Mechanics.

I just twice effectively used ChatGPT to analyze your own conspiratorial posts, which seems to have pissed you off as if ChatGPT was being unfair to you, which is why it's so special that you've now flip-flopped into endorsing the use of LLMs to debug code, while on the same day you were so taken aback when somebody simply and effectively uses them to debug and analyze your own bullshit, and then an actual quantum scientist chimes in to agree with "the paid GPT4 that's much smarter" and strongly disagree with you too.

If you don't like your arguments being criticized by an LLM, then how do you feel about the criticism from an actual scientist, and why do you advocate having LLMs criticize your own code? Do you get just as angry at ChatGPT when it criticizes your code, as you do when it criticizes your logical fallacies about Quantum Mechanics? It's just a computer, you know, so your rage is misplaced. I hope you can debug your code better than you can debug your conspiracy theories, instead of clinging to them even tighter in the face of valid criticism. You must be fun at code reviews!

https://news.ycombinator.com/item?id=39376510

>jiggawatts 12 hours ago [flagged] | parent | context | flag | favorite | on: Inside the proton, the ‘most complicated thing you...

>Quantum mechanics is a religion with mathematics instead of just holy texts.

[...Gish Gallop of invalid arguments in your "[flagged]" posting redacted...]

https://news.ycombinator.com/item?id=39378453

>DonHopkins 8 hours ago | prev [–]

>It's really easy to spout bullshit like that, if you have absolutely no idea what you're talking about, and you're just trying to carry the water for religion by unfairly accusing science of having religion's fundamental flaws.

>It's a veritable Gish Gallop of logical fallacies:

>False Analogy: The argument compares quantum mechanics (QM) to religion, stating that both involve factions, orthodoxy, and unchallengeable beliefs. However, this is a false analogy because the nature and methods of scientific inquiry (e.g., empirical evidence, peer review, falsifiability) are fundamentally different from those of religious belief (which is based on faith and doctrine). The comparison oversimplifies and misrepresents both science and religion.

>Strawman Fallacy: The argument misrepresents the nature of quantum mechanics by suggesting that it operates purely on faith or dogma, similar to religious belief. This ignores the extensive empirical and theoretical work that underpins quantum mechanics.

>Ad Hominem (Circumstantial): The argument suggests that scientists who work in the field of QM are practicing a form of religious devotion rather than scientific inquiry. This is an ad hominem attack because it attempts to discredit QM by attacking the motives or character of its practitioners, rather than addressing the scientific validity of the field itself.

>Hasty Generalization: The argument makes broad generalizations about quantum mechanics and its practitioners based on limited observations (e.g., some disagreements among physicists). Scientific disagreements are a normal part of the scientific process and do not necessarily imply that the entire field is akin to a religion.

>Appeal to Ignorance (Argumentum ad Ignorantiam): The argument implies that because some aspects of QM (like wave-particle duality) seem counterintuitive or hard to comprehend, they must therefore be nonsensical or based on faith. This is an appeal to ignorance, as it suggests a lack of understanding or evidence is equivalent to proof of the argument's correctness.

>Overgeneralization/Sweeping Generalization: The argument overgeneralizes the behavior of scientific communities, suggesting that all scientific disagreements lead to "warring factions" and are akin to religious schisms. This overlooks the nuanced and varied ways in which scientific communities debate, test, and revise theories.

>No True Scotsman: By defining 'true' science as being free of disagreements or factions (and suggesting QM doesn't meet this standard), the argument potentially commits a No True Scotsman fallacy, where arbitrary criteria are set up to define what 'real' science should look like.

https://news.ycombinator.com/item?id=39379328

>jiggawatts 6 hours ago [flagged] [dead] | parent [–]

[...apoplectic attempt at point by point rebuttal in your "[flagged] [dead]" posting redacted, followed by emotional attack on me using ChatGPT to school you by analyzing and enumerating your mistakes...]

>It boils down to this: I don't even have to know how to do a thing myself to recognise that other people don't know either. If two of them disagree on matters of fact, one of them is wrong. If many of them disagree in many ways, more than likely they are all wrong. This same criticism is popularly levelled against religions (plural!) of which there are many mutually exclusive variants, even within one main branch such as Islam or Christianity. They regularly kill each other over such disagreements, such as Shia vs Sunni or Protestant vs Catholic.

>You're saying I shouldn't criticise this.

>On what basis do you think that?

>Or did ChatGPT think this for you?

https://news.ycombinator.com/item?id=39379755

>bowsamic 4 hours ago | unvote | parent | context | flag | favorite | on: Inside the proton, the ‘most complicated thing you...

>I’m really confused here as a quantum physicist myself. Yes there is huge disagreement and yes it’s a problem, but also what is the alternative? It’s not like we can just give up on quantum mechanics because you personally have philosophical problems with it. My task is to reduce the fundamental quantum noise that we see in gravitational wave detectors after removing all the classical noise. How would it be constructive to just say “let’s pretend there is no quantum noise?”

>To me it’s exciting that there is no clear interpretation for quantum mechanics, and it also nicely retroactively casts doubt on our interpretation for all previous theories: did classical mechanics just coincidentally present as deterministic? Etc. maybe you think questions about determinism are woo but I think that would be quite extreme

>Honestly, I don’t see why it’s a problem that there are different interpretations of quantum mechanics

https://news.ycombinator.com/item?id=39381147

>DonHopkins 13 minutes ago | edit | delete [–]

>He's apoplectic that ChatGPT was able to cut through his bluster and bullshit and enumerate his Gish Gallop of logical fallacies like a hot knife cutting through butter. If it stings so much, then maybe he should first run his own ridiculous conspiracy theories and baseless accusations against science and false equivalencies about religion through ChatGPT himself before posting them here, to strengthen them up and educate himself, instead of embarrassing himself by being so thoroughly and effectively schooled by a mere LLM and an actual quantum physicist.

>Original Argument:

>Quantum Mechanics as Religion: Quantum mechanics (QM) is likened to a religion, with disagreements among physicists, an orthodox Copenhagen interpretation, and adherence to seemingly nonsensical concepts like wave-particle duality.

>Logical Fallacies and Mistakes:

>False Analogy: Comparing QM to religion overlooks fundamental differences in methodologies and goals. Science is empirical and self-correcting; religion is based on faith.

>Strawman Fallacy: Misrepresents QM as purely faith-based or dogmatic. QM is grounded in empirical evidence and rigorous mathematics.

>Ad Hominem: Attacks the character or motives of QM practitioners, rather than addressing the scientific validity of QM itself.

>Hasty Generalization: Overgeneralizes from disagreements among physicists to claim the entire field is unscientific.

>Appeal to Ignorance: Assumes that because aspects of QM are counterintuitive, they must be nonsensical or faith-based.

>Overgeneralization/Sweeping Generalization: Claims that disagreements in QM are indicative of flaws in all scientific fields, ignoring the diversity and complexity of scientific disciplines.

>No True Scotsman: Imposes arbitrary criteria for what constitutes 'real' science, excluding QM based on its interpretive disagreements.

>Validity of Arguments:

>Limited Validity in Recognizing Disagreements: The argument validly recognizes the existence of disagreements and different interpretations within QM, which is a natural aspect of any evolving scientific field.

>Misinterpretation of Nature of Science: However, the argument fails to appreciate the empirical basis of science and the role of theoretical diversity in scientific progress.

>Rebuttal from an Actual Scientist:

>Quantum Mechanics as a Practical and Evolving Science: The scientist highlights the practical applications of QM, the excitement of unresolved questions, and the evolving nature of scientific understanding.

>Assessment of Rebuttal:

>Practicality and Utility: The rebuttal correctly emphasizes the practical applications of QM, which are well-established and empirically validated.

>Scientific Progress and Open Questions: The scientist’s view of the unresolved aspects of QM as exciting and valuable is in line with the nature of scientific inquiry, which thrives on exploration and continuous refinement.

>Conclusion:

>The original argument conflates the philosophical and interpretative aspects of QM with religious belief, using several logical fallacies. It overlooks the empirical foundation and practical success of QM.

>The rebuttal from the scientist provides a more accurate representation of QM as a practical, empirically grounded, and continuously evolving field of science. The existence of different interpretations and unresolved questions is not a flaw but a driving force for further research and understanding.

Plus it totally contradicts you assertions above about the usefulness of Google and ChatGPT. Flip, flop, flip, flop!

You could at least have the integrity and intellectual honesty to reply directly to the actual real live scientist, a professional quantum physicist, who took the time to correctly rebut your wild conspiracy theories and gross misunderstandings of science, but you chose not to, and the crickets are still chirping away, awaiting your response.

But your lack of a response to him says so much more about you than your response possibly could (short of an admission that you are wrong and an apology for attacking scientists and a promise to do better next time).

Do you see the irony? Nope. You just contradicted yourself and flip-flopped yet again, reflexively clinging to your anti-scientific conspiracy theories even tighter, as revenge for being called out with the facts by a professional scientist, just like any dime-a-dozen foaming-at-the-mouth Q-Anon freak would. That only makes you even more wrong and ridiculous looking, and doesn't hurt or fool anybody else.

"what’s surprising is that physicists seem to be O.K. with not understanding the most important theory they have."

Sean Carroll (2019): https://www.nytimes.com/2019/09/07/opinion/sunday/quantum-ph...

I don't think the guy you are at war with deserves so much attention and energy on your part. Not only is the point he's making not that different from what I linked above, although I reckon he gave it an arrogant spin, but the way you react somehow vindicates the parallels he established between science and religion. Not sure how Q-Anon is related to all of this.

The usefulness of LLMs for writing code is strongly correlated with how "Stack Overflowable" your work is.

Just wanted to remind people that we haven't sucked the human element out of math.

This to me is one of the exciting core capabilities that AI unlocks: the ability to verify/enforce a set of standards across many inputs. It's one of the information age's core problems. One example used a lot in social sciences is inter-rater reliability (IRR) [1]. There's probably a lot of domains out there that can benefit from this pattern of machines verifying distributed human inputs, both in crunch the numbers like machine assisted proofs, as well as more subjective domains where subjectivity can be extremely carefully defined.

I'd love to see more AI tooling focused on these kinds of large scale multi-contributor problem solving methods, including the idea of knowing how to correctly state the overall problem (I believe this was an example in the video).

[1] https://en.wikipedia.org/wiki/Inter-rater_reliability

The ITPs will keep the LLMs in check, and stop them from bs-ing.

The ITPs unlock massive collaboration.

Edit: are they interactive theorem provers?

I tried to teach GPT about an algorithm I come up with to run a sequence of min-heap operations in O(n) (instead of O(n log n)). But I could not make it understand. But that was also a brand new concept built on top of some pretty niche literature (Chazelle's Soft Heap); so GPT would have to actually 'think', instead of just regurgitate papers.

My prompt was: (and it gave me the right answer)

"I have to formulate an MIP. I have a list of items i \in I each belong to groups g \in G. They are related by a static parameter G_{ig} which says if i in g, then 1 else 0. I want each item i to be freely and independently assigned to slots c \in C. However I want to keep items i together with other items in the same group if possible -- it's a soft preference.

How do i write the mathematical MIP formulation?"

I've been wanting to build a tool to help find and work with combos for deck builders of card games -- specifically Magic: The Gathering, but it could also apply to other games.

There is a wonderful dataset of combos available for download from Commander Spellbook -- currently boasting over 26k combos in the database, and growing all the time.

One thought I've had is to train my own embedding model so that cards that are likely to combo with each other embed closely with one other. This way, even after new cards are printed, we can rapidly discover cards that are likely to combo with them. In practice, the first attempt that I had at fine-tuning my own embedding model proved lackluster, but I intend to refine my data and try again -- possibly after pre-training.

Second thought is to fine-tune an LLM on the text of existing combos -- give it the text of each card in the combo, and then train it to predict the rest of the interactions. This is cool and all, but I don't entirely know how to train it to (reliably) give "these cards don't combo" answers -- I fear that it would tend to hallucinate for cards that don't combo, and I don't know how to handle that.

Obviously any answers that come out of this system would need to be vetted by humans before adding to the database, but it feels like this could be an interesting way to explore the game space if nothing else.

In a related way, it feels like a mathematical proof begins with a set of starting conditions, a conjecture, and then works forward using established rules. In a similar way, a combo in Magic starts with a set of starting conditions, a conjecture ("this combo will result in infinite life" or "this combo will result in infinite damage"), and then works forward to detail the process of using established rules to accomplish the conjecture.

Anyways, it's an interesting use-case to me, and I'm excited to learn more about the parallels. I don't know if my embedding model or my LLM approach are worthwhile, and I would like to learn about other tactics I might employ!

But can we do even better? Terence touches upon automated theorem proving, which to some degree formalizes the notion of searching proof space. Once formalized, this becomes its own area of mathematics, where now the goal is to find proofs of the fastest ways to search the subset of proofs relevant to fast proof-finding.

It’s always been a bit odd to me that we defaulted to considering probabilistic approaches to universal search rather than mathematical ones; these are all mathematical structures at the core of it after all, so I would think deduction would be much more effective than induction in this domain. But then again, who knows—GPT seems to be quickly getting better at providing novel intuitive ideas to explore. And I guess induction is actually kind of necessary when determining which potential path of deduction to explore.

Another question is whether there exist algorithms that are the most efficient at solving particular classes of problems but unprovably so within any reasonable formal system, in which case automated theorem proving wouldn’t help. I kind of doubt it though. And in that case, brute-force search certainly isn’t going to find those algorithms either, so they may as well not exist within our “lightcone” of reachable algorithms that could be used to accelerate universal search.

The only exception would be if these algorithms do exist and are actually dense in program space—in that case I suppose you would then have to optimize the balance of time spent between searching proof space and algorithm space. Again, I would intuitively think this possibility is highly unlikely, and so we should instead spend all of our time on improving machine assisted proof systems if we want to accelerate AI development via improvements to universal search.

Love that my name appears in the talk (in small print) :-D

Now I just have to somehow find funding for my project, Practal [1].

[1] https://practal.com

Since formal proof checkers provide a reward signal (correct/incorrect proof) the above process could scale to superhuman performance in generating proofs for conjectures. This is unlike ordinary language models, which only try to imitate the human-written training distribution.