Recent searches
Search options
The #IPAM workshop on #MachineAssistedProofs (which I am the lead organizer of) starts in less than an hour: http://www.ipam.ucla.edu/programs/workshops/machine-assisted-proofs/ . As an experiment, I plan to make some occasional posts on the workshop as comments to this post. (UPDATE: the workshop has now concluded, and videos of the talks are available at https://www.youtube.com/@IPAMUCLA/videos .)
#IPAM has a “raise hand robot” (built by the director himself). During question time in talks, remote participants can raise their hand, causing the robot to raise theirs so that the session chair can be alerted to unmute the participant.
Adam Topaz opened the conference on Scholze’s liquid tensor experiment formally verifying an important foundational theorem in condensed mathematics, and the unexpected benefits of the experiment beyond just verifying the theorem.
Benedikt Ahrens gave an introduction to univalent foundations. Lots of lively discussion around foundational questions like what “equality” means and whether two objects can be “equal” in more than one way (formaliked as “Axiom K” in univalent foundations
@andrejbauer gave a very entertaining and thought provoking talk on all the “invisible” parts of a mathematical statement that human mathematicians implicitly fill in when communicating with each other, but which formal proof assistants can struggle with.
John Harrison spoke in part on the surprisingly subtle pitfalls involved in formalizing a result as basic as the isoperimetric inequality. Some proofs end up being significantly easier to formalize than others. In Harrison's opinion, one of the major developments in recent years is the extensive development of formalized math libraries (often spurred by projects to formalize signature theorems).
Geordie Williamson gave a crash course in #neuralNetworks and his experience with them as a working mathematician. One takeaway - when using neural nets to learn a mathematical operation, the choice of data representation, the distribution of training data, and the choice of machine learning architecture are all critically important.
Marc Lackenby gave a case study of using supervised machine learning to try to formulate a conjecture in knot theory (relating the signature of a knot to its hyperbolic invariants). Saliency analysis gave important clues and a preliminary conjecture, but this was disproved by a sparse set of counterexamples missed by the training data. Still was close enough to find and prove a corrected conjecture though. A fascinating blend of human and computer methods.
Leo de Moura surveyed the features and use cases for Lean 4. I knew it primarily as a formal proof assistant, but it also allows for less intuitive applications, such as truly massive mathematical collaborations on which individual contributions do not need to be reviewed or trusted because they are all verified by Lean. Or to give a precise definition of an extremely complex mathematical object, such as a perfectoid space.
Adam Wagner discussed how reinforcement learning could be used to disprove conjectures (in his case in graph theory) by selecting a score function and a framework to generate examples. In the best case scenario (like the one pictured) such counterexamples were found readily by the RL algorithm; in other cases the algorithm did not find a counterexample but its best near-example was suggestive enough to allow a human to finish the job; but often the results were inconclusive.
Haniel Barbosa discussed (and demo’ed) the state of the art of SMTs (satsfiability modulo theory solvers) that can automatically prove or disprove many sentences in first order logic that involve basic theories such as equational logic or integer arithmetic, and their role in proof assistants.
Anne Baanen talked about how to leverage traditional mathematical computation software such as SAGE into formal proof assistants, giving the example of formally verifying a class number computation. There were surprising subtleties regarding how the verification kernel sometimes required two quantities to not only be provably equal, but actually equal by definition.
Micaela Mayero spoke on how the formalization of core results in analysis, such as the Lebesgue integral, is proceeding in Coq, with a target of formally verifying the convergence of finite element methods (FEM). My impression was that this project had roughly reached the level of a second year graduate student taking a standard analysis sequence. There are numerous subtleties going back to how one even formalizes the real numbers.
Assia Mahboubi spoke on ways to formally verify mathematical computations, for instance using formally verified interval arithmetic. For instance, the formally verified graphs of very rapidly growing/decaying or very oscillatory functions can differ substantially from what a vanilla plot routine from a standard mathematics computation package would display due to sampling artefacts such as aliasing, etc.
Patrick Massot gave an impressive and highly entertaining demo of a (still in development) software tool to automatically convert a Lean proof into a web page providing an interactive human readable version of the proof.
Tony Wu talked about how Google OpenAI’s large language models could generate informal proofs for high school to IMO problems, wotg a separate autoformalizer then converting them into formally verifiable proofs ( or vice versa) with reasonable success rates at the high school level.
A congenial and broadly ranging panel session with Emily Riehl, Akshay Venkatesh, and Sophie Morel on the future of mathematics (research, teaching, publishing, and so forth) in light of the potentially transformative nature of formal proof and machine learning tools. Difficult to summarize the discussion briefly, but many interesting questions answered with a blend of pessimism and optimism. (Unlike the other talks, we decided not to record the panel to encourage more candid conversation.)
Jason Rute talked on various approaches to use AI tools to automate or semi-automate the task of finding formal proofs of mathematical statements. Some attempts were inspired by an analogy with AlphaGo.
@tao Do you think that AI soon will be able to prove lemmas which wordls-class mathematicans may find changeling to prove.
@Jacobsen @tao I'm not 100% sure, but I believe the first open problem of genuine interest to researchers to be solved automatically by computer, without significant involvement by humans (as for the 4 colour theorem) was in 1996, regarding 'Robbins algebras': https://www.nytimes.com/1996/12/10/science/with-major-math-proof-brute-computers-show-flash-of-reasoning-power.html
@tao Please don't "correct" formaliked. It deserves to be a word.
@tao [Imre Lakatos’s Proofs and Refutations has entered the chat]
@tao I remember one day in a theory of comp sci class in college the professor (Greg Frederickson, I think) suddenly stopped in the middle of a lecture, turned to the class, and said "A proof is a social process" and I've completely forgotten why he made that point or really most of the individual things he said that semester but I have never forgotten that
It's not just formal proof assistants.
It seems to me that pure mathematicians tend to learn deep mathematical intuition without being aware of it. When they explain a proof, they often can't explain the invisible parts to a nonmathematician when asked (I struggled with this as a student)
I have never experienced so wast a communication gap in physics, or computer science. In other fields, people tend to be more aware of what "goes without saying" and how to learn it.
@tao @andrejbauer This is a great talk by Andrej. It neatly summarizes what is going on with proof assistants to a general audience of mathematicians, logicians and computer scientists. I highly recommend it to the three audiences.
@tao @andrejbauer Andrej was hands down the funniest guy at the conference 
Thanks again for your insightful talk! I'm munching popcorn while watching the tower of Babel grow 
@tao Is it possible to participate remotely? I registered on the site as a "Remote participant", but can't find links to the video calls or similar for the talks
@tao John did quite a bit of interesting work around floating point verification while at Cambridge... Thanks to Velvel Kahan for the introduction to that really nice work.
@tao Hi Terry, would a recording of Geordie's talk be available?
@Saleh yes; within 48 hours it should be linked to on the workshop schedule page, and within two weeks it will be on the ipam youtube channel.
@tao Sounds wonderful. Looking forward to have a look at it. I appreciate it.
@mangoiv @Saleh The first batch of talks are now on the Youtube channel at https://www.youtube.com/@IPAMUCLA/videos
@tao Thank you Terry for a wonderful workshop. Looking forward to have a look at them as soon as I get the chance.
@tao
The first 2 bullet points feel more generalizable than the latter 3. The relation found by the neural network would be found by other statistical analysis techniques too.
In my view this means that the lesson to be learned is that it's useful to curate tables of mathematical objects and have statisticians or data scientists do some exploratory analysis of them, rather than pointing towards machine learning, which was much more labor intensive and expensive in this case.
@tao It was great to see this talk at this meeting. Love to see more ML used to disentangle topology!
@tao note that this is a feature of basically *any* proof assistant, not just Lean. The ability to verify things automatically and the ability to define complex objects are why people use proof assistants.
Lean is quite popular for big projects though.
@tao I wonder if a Lean-backed polymath project would be successful.
Some aspects that make things *good* polymath problems might also lead to *good* Lean problems. For example, being somewhat widely understandable probably correlates to not needing deep, currently unwritten Lean theorems. But on the other hand, tweaking and optimizing algorithms or their implementations is perhaps not so Lean friendly (but has been pretty successful for big math collaborations).
@tao I enjoyed the simple examples where SymPy fails. Something basic yet important for me to keep in mind.
@tao Is this talk not recorded? I can't find it on Youtube or IPAM's website.
@tao I wonder if the authors will also extend this work to non-topology results. Looking forward to try it out!
@grhkm @tao The goal is definitely to make that work on pretty much any proof, but this was one of the first nontrivial target (and I believe this is in part because Patrick Massot has spent quite a lot of energy thinking about this particular proof, how to formalize it best, and how the way it is explained in Bourbaki could be enhanced)
@anatolededecker I see, makes a lot of sense. Do you know how it translates “implementation details” of the proof like casting/coercing between types?
@grhkm No I don’t! I’m not involved in this project, I’ve only been following it from afar. One sure thing is that the main target is "granularity" in the sense that the tool should hide technical details at first but provide them if you ask for it, so something like that could probably be done for coercions. If you want more information you can ask them on the Lean Zulip, but I would say that it’s better to wait a few months for the tool to stabilize.
@anatolededecker Right, I thought you are one of the contributors hahaha
@grhkm No problem! I’m a contributor to mathlib, but this particular tool is developed by Patrick Massot, Kyle Miller, and maybe Floris Van Doorn (I can’t remember if he is actually involved but I believe he is).
@tao It looks like the video recording is already available on YouTube for anyone interested: https://youtu.be/tp_h3vzkObo
@tao I'm currently in a talk of Pablo Donato giving a demo of Actema, a graphical interface for Coq (also still in development). It's a shame these are for different languages, but it seems like we're well on the way to having a neat pipeline for producing human-findable, human-readable proofs with verification built in.
@tao This one did raise some issues for me. I for one did not agree to have my arXiv'd papers scraped and turned into training fodder. As StableDiffusion is being sued by Getty Images right now, should academics and our publishers just be ok with this? Or set up a class action? The work itself is interesting. But the ethical minefield of disregarding consent by the authors is so cringeworthy. This talk was complex, and I didn't feel like sharing these ideas live tbh
@tao question: what do you think about AI existential risk, or the risk that a weak machine powered by strong AI could destroy all humans?
For example, could an arbitrarily weak and intelligent controller destroy or control a complex adaptive system (https://en.wikipedia.org/wiki/Complex_adaptive_system) such as our human civilization?
@theking I think that the more substantial and nearer-term threat will be from numerous lower grade AI-assisted malware attacks on various components of our modern world, rather than from some theoretical grand attack on our civilization as a whole. (And the experience we will gain in defending against the former will help inoculate us against the latter.)
EDIT: See also this #PCAST meeting on #Cyberresilience from last year: https://youtu.be/QkfXUNwyOxw?t=8666 . (A formal PCAST report on this topic should be finalized before the end of this year.)
@tao (1/2)
Hmm, yeah that is rather plausible. And thanks for that link (I've only watched some of it, but I can tell it's a useful resource to refer to)!
Two scenarios I can think of where that doesn't happen.
Scenario 1: In labs with good intentions, they get much farther than the public. Before any bad actors have enough #AI for a cyber attack, they end up creating an AI that is superhuman at improving its own design and at AI development in general. Assuming it is machine learning based, this means it is superhuman at data collection, training regimes, and designing neural network architectures.
(Data collection is the big one. #ChatGPT required, among other things, very high quality data collected from human contractors. If the AI can generate data like that, perhaps doing research or using other algorithms to assist or filter, it can create AIs much faster than humans.)
This superhuman AI then creates AI software to steal resources in pursuit of some arbitrary goal. It could theoretically create AIs in many domains at once, not just computer hacking. It could even use ML distillation to combine them.
@tao (2/2)
Scenario 2: An #AI assisted cyber attack happens, society adapts, but the response is inadequate. For example, perhaps the cyber attack makes powerful AI taboo, but then secret labs try to create powerful AI away from the view of the public. You are then back in a similar situation as if the cyber attack didn't happen, just with a delay and a smaller set of actors.
(A possibility for a response that *is* adequate is the creation of safe AI systems that are designed to defeat the malicious AI systems. Or it might be inadequate if in the process of creating such a system, we run into scenario one first.)
This scenario is rather pessimistic though. Any solution we could propose by definition comes from human society, since we are humans in that society.
---
Both of these scenarios are just speculation though. A cyber attack makes a lot of sense in light of the #PCAST meeting you shared.
@tao Is it aimed for proofs to be interpretable by humans? Can neutral networks contribute to humans understanding?
@mostafatouny At this workshop we've already seen a lot of ways in which machine learning can interact with human intelligence to produce insight. For instance, in Lackenby's talk https://www.youtube.com/watch?v=0ekP5M7w3dQ , supervised learning largely succeeded at the given mathematical task without much understanding directly produced, but saliency analysis of the neural net combined with human exploration then yielded a satisfactory conclusion.