Just a short post to advertise the workshop “Machine assisted proofs” that will be held on Feb 13-17 next year, here at the Institute for Pure and Applied Mathematics (IPAM); I am one of the organizers of this event together with Erika Abraham, Jeremy Avigad, Kevin Buzzard, Jordan Ellenberg, Tim Gowers, and Marijn Heule. The purpose of this event is to bring together experts in the various types of formal computer-assisted methods used to verify, discover, or otherwise assist with mathematical proofs, as well as pure mathematicians who are interested in learning about the current and future state of the art with such tools; this seems to be an opportune time to bring these communities together, given some recent high-profile applications of formal methods in pure mathematics (e.g, the liquid tensor experiment). The workshop will consist of a number of lectures from both communities, as well as a panel to discuss future directions. The workshop is open to general participants (both in person and remotely), although there is a registration process and a moderate registration fee to cover costs and to restrict the capacity to genuine applicants.

### Recent Comments

tt on A Host–Kra F^omega_2-sys… | |

Joe Smith on Mathematics for Humanity initi… | |

Michael Ruxton on A counterexample to the period… | |

KEW on Equidistribution of Syracuse r… | |

a on A Host–Kra F^omega_2-sys… | |

Alison Playle on A new proof of the density Hal… | |

Alison Playle on A new proof of the density Hal… | |

Anonymous on A new proof of the density Hal… | |

Anonymous on A new proof of the density Hal… | |

a on A Host–Kra F^omega_2-sys… | |

Anonymous on A Host–Kra F^omega_2-sys… | |

Arman on A Host–Kra F^omega_2-sys… | |

Solomon Ucko on There’s more to mathematics th… | |

Eric Naslund on Density Hales-Jewett and Moser… | |

Eric Naslund on Density Hales-Jewett and Moser… |

### Articles by others

- Andreas Blass – The mathematical theory T of actual mathematical reasoning
- Gene Weingarten – Pearls before breakfast
- Isaac Asimov – The relativity of wrong
- Jonah Lehrer – Don't! – the secret of self-control
- Julianne Dalcanton – The cult of genius
- Nassim Taleb – The fourth quadrant: a map of the limits of statistics
- Paul Graham – What You'll Wish You'd Known
- Po Bronson – How not to talk to your kids
- Scott Aaronson – Ten signs a claimed mathematical proof is wrong
- Tanya Klowden – articles on astronomy
- Timothy Gowers – Elsevier — my part in its downfall
- Timothy Gowers – The two cultures of mathematics
- William Thurston – On proof and progress in mathematics

### Diversions

- Abstruse Goose
- BoxCar2D
- Factcheck.org
- Gapminder
- Literally Unbelievable
- Planarity
- PolitiFact
- Quite Interesting
- snopes
- Strange maps
- Television tropes and idioms
- The Economist
- The Onion
- The Straight Dope
- This American Life on the financial crisis I
- This American Life on the financial crisis II
- What if? (xkcd)
- xkcd

### Mathematics

- 0xDE
- A Mind for Madness
- A Portion of the Book
- Absolutely useless
- Alex Sisto
- Algorithm Soup
- Almost Originality
- AMS blogs
- AMS Graduate Student Blog
- Analysis & PDE
- Analysis & PDE Conferences
- Annoying Precision
- Area 777
- Ars Mathematica
- ATLAS of Finite Group Representations
- Automorphic forum
- Avzel's journal
- Blog on Math Blogs
- blogderbeweise
- Bubbles Bad; Ripples Good
- Cédric Villani
- Climbing Mount Bourbaki
- Coloquio Oleis
- Combinatorics and more
- Compressed sensing resources
- Computational Complexity
- Concrete nonsense
- David Mumford's blog
- Delta epsilons
- DispersiveWiki
- Disquisitiones Mathematicae
- Embûches tissues
- Emmanuel Kowalski’s blog
- Equatorial Mathematics
- fff
- Floer Homology
- Frank Morgan’s blog
- Gérard Besson's Blog
- Gödel’s Lost Letter and P=NP
- Geometric Group Theory
- Geometry and the imagination
- Geometry Bulletin Board
- George Shakan
- Girl's Angle
- God Plays Dice
- Good Math, Bad Math
- Graduated Understanding
- Hydrobates
- I Can't Believe It's Not Random!
- I Woke Up In A Strange Place
- Igor Pak's blog
- Images des mathématiques
- In theory
- James Colliander's Blog
- Jérôme Buzzi’s Mathematical Ramblings
- Joel David Hamkins
- Journal of the American Mathematical Society
- Keith Conrad's expository papers
- Kill Math
- Le Petit Chercheur Illustré
- Lemma Meringue
- Lewko's blog
- Libres pensées d’un mathématicien ordinaire
- LMS blogs page
- Low Dimensional Topology
- M-Phi
- Mark Sapir's blog
- Math Overflow
- Math3ma
- Mathbabe
- Mathblogging
- Mathematical musings
- Mathematics Illuminated
- Mathematics in Australia
- Mathematics Jobs Wiki
- Mathematics Stack Exchange
- Mathematics under the Microscope
- Mathematics without apologies
- Mathlog
- Mathtube
- Matt Baker's Math Blog
- Mixedmath
- Motivic stuff
- Much ado about nothing
- Multiple Choice Quiz Wiki
- MyCQstate
- nLab
- Noncommutative geometry blog
- Nonlocal equations wiki
- Nuit-blanche
- Number theory web
- Online Analysis Research Seminar
- outofprintmath
- Pattern of Ideas
- Pengfei Zhang's blog
- Persiflage
- Peter Cameron's Blog
- Phillipe LeFloch's blog
- ProofWiki
- Quomodocumque
- Ramis Movassagh's blog
- Random Math
- Reasonable Deviations
- Regularize
- Research Seminars
- Rigorous Trivialities
- Roots of unity
- Science Notes by Greg Egan
- Secret Blogging Seminar
- Selected Papers Network
- Sergei Denisov's blog
- Short, Fat Matrices
- Shtetl-Optimized
- Shuanglin's Blog
- Since it is not…
- Sketches of topology
- Snapshots in Mathematics !
- Soft questions
- Some compact thoughts
- Stacks Project Blog
- SymOmega
- Tanya Khovanova's Math Blog
- tcs math
- TeX, LaTeX, and friends
- The accidental mathematician
- The Cost of Knowledge
- The Everything Seminar
- The Geomblog
- The L-function and modular forms database
- The n-Category Café
- The n-geometry cafe
- The On-Line Blog of Integer Sequences
- The polylogblog
- The polymath blog
- The polymath wiki
- The Tricki
- The twofold gaze
- The Unapologetic Mathematician
- The value of the variable
- The World Digital Mathematical Library
- Theoretical Computer Science – StackExchange
- Thuses
- Tim Gowers’ blog
- Tim Gowers’ mathematical discussions
- Todd and Vishal’s blog
- Van Vu's blog
- Vaughn Climenhaga
- Vieux Girondin
- Visual Insight
- Vivatsgasse 7
- Williams College Math/Stat Blog
- Windows on Theory
- Wiskundemeisjes
- XOR’s hammer
- Yufei Zhao's blog
- Zhenghe's Blog

### Selected articles

- A cheap version of nonstandard analysis
- A review of probability theory
- American Academy of Arts and Sciences speech
- Amplification, arbitrage, and the tensor power trick
- An airport-inspired puzzle
- Benford's law, Zipf's law, and the Pareto distribution
- Compressed sensing and single-pixel cameras
- Einstein’s derivation of E=mc^2
- On multiple choice questions in mathematics
- Problem solving strategies
- Quantum mechanics and Tomb Raider
- Real analysis problem solving strategies
- Sailing into the wind, or faster than the wind
- Simons lectures on structure and randomness
- Small samples, and the margin of error
- Soft analysis, hard analysis, and the finite convergence principle
- The blue-eyed islanders puzzle
- The cosmic distance ladder
- The federal budget, rescaled
- Ultrafilters, non-standard analysis, and epsilon management
- What is a gauge?
- What is good mathematics?
- Why global regularity for Navier-Stokes is hard

### Software

### The sciences

### Top Posts

- Career advice
- A Host--Kra F^omega_2-system of order 5 that is not Abramov of order 5, and non-measurability of the inverse theorem for the U^6(F^n_2) norm; The structure of totally disconnected Host--Kra--Ziegler factors, and the inverse theorem for the U^k Gowers uniformity norms on finite abelian groups of bounded torsion
- Does one have to be a genius to do maths?
- There’s more to mathematics than rigour and proofs
- Books
- On writing
- Work hard
- About
- The Euler-Maclaurin formula, Bernoulli numbers, the zeta function, and real-variable analytic continuation
- A new proof of the density Hales-Jewett theorem

### Archives

- March 2023 (2)
- February 2023 (1)
- January 2023 (2)
- December 2022 (3)
- November 2022 (3)
- October 2022 (3)
- September 2022 (1)
- July 2022 (3)
- June 2022 (1)
- May 2022 (2)
- April 2022 (2)
- March 2022 (5)
- February 2022 (3)
- January 2022 (1)
- December 2021 (2)
- November 2021 (2)
- October 2021 (1)
- September 2021 (2)
- August 2021 (1)
- July 2021 (3)
- June 2021 (1)
- May 2021 (2)
- February 2021 (6)
- January 2021 (2)
- December 2020 (4)
- November 2020 (2)
- October 2020 (4)
- September 2020 (5)
- August 2020 (2)
- July 2020 (2)
- June 2020 (1)
- May 2020 (2)
- April 2020 (3)
- March 2020 (9)
- February 2020 (1)
- January 2020 (3)
- December 2019 (4)
- November 2019 (2)
- September 2019 (2)
- August 2019 (3)
- July 2019 (2)
- June 2019 (4)
- May 2019 (6)
- April 2019 (4)
- March 2019 (2)
- February 2019 (5)
- January 2019 (1)
- December 2018 (6)
- November 2018 (2)
- October 2018 (2)
- September 2018 (5)
- August 2018 (3)
- July 2018 (3)
- June 2018 (1)
- May 2018 (4)
- April 2018 (4)
- March 2018 (5)
- February 2018 (4)
- January 2018 (5)
- December 2017 (5)
- November 2017 (3)
- October 2017 (4)
- September 2017 (4)
- August 2017 (5)
- July 2017 (5)
- June 2017 (1)
- May 2017 (3)
- April 2017 (2)
- March 2017 (3)
- February 2017 (1)
- January 2017 (2)
- December 2016 (2)
- November 2016 (2)
- October 2016 (5)
- September 2016 (4)
- August 2016 (4)
- July 2016 (1)
- June 2016 (3)
- May 2016 (5)
- April 2016 (2)
- March 2016 (6)
- February 2016 (2)
- January 2016 (1)
- December 2015 (4)
- November 2015 (6)
- October 2015 (5)
- September 2015 (5)
- August 2015 (4)
- July 2015 (7)
- June 2015 (1)
- May 2015 (5)
- April 2015 (4)
- March 2015 (3)
- February 2015 (4)
- January 2015 (4)
- December 2014 (6)
- November 2014 (5)
- October 2014 (4)
- September 2014 (3)
- August 2014 (4)
- July 2014 (5)
- June 2014 (5)
- May 2014 (5)
- April 2014 (2)
- March 2014 (4)
- February 2014 (5)
- January 2014 (4)
- December 2013 (4)
- November 2013 (5)
- October 2013 (4)
- September 2013 (5)
- August 2013 (1)
- July 2013 (7)
- June 2013 (12)
- May 2013 (4)
- April 2013 (2)
- March 2013 (2)
- February 2013 (6)
- January 2013 (1)
- December 2012 (4)
- November 2012 (7)
- October 2012 (6)
- September 2012 (4)
- August 2012 (3)
- July 2012 (4)
- June 2012 (3)
- May 2012 (3)
- April 2012 (4)
- March 2012 (5)
- February 2012 (5)
- January 2012 (4)
- December 2011 (8)
- November 2011 (8)
- October 2011 (7)
- September 2011 (6)
- August 2011 (8)
- July 2011 (9)
- June 2011 (8)
- May 2011 (11)
- April 2011 (3)
- March 2011 (10)
- February 2011 (3)
- January 2011 (5)
- December 2010 (5)
- November 2010 (6)
- October 2010 (9)
- September 2010 (9)
- August 2010 (3)
- July 2010 (4)
- June 2010 (8)
- May 2010 (8)
- April 2010 (8)
- March 2010 (8)
- February 2010 (10)
- January 2010 (12)
- December 2009 (11)
- November 2009 (8)
- October 2009 (15)
- September 2009 (6)
- August 2009 (13)
- July 2009 (10)
- June 2009 (11)
- May 2009 (9)
- April 2009 (11)
- March 2009 (14)
- February 2009 (13)
- January 2009 (18)
- December 2008 (8)
- November 2008 (9)
- October 2008 (10)
- September 2008 (5)
- August 2008 (6)
- July 2008 (7)
- June 2008 (8)
- May 2008 (11)
- April 2008 (12)
- March 2008 (12)
- February 2008 (13)
- January 2008 (17)
- December 2007 (10)
- November 2007 (9)
- October 2007 (9)
- September 2007 (7)
- August 2007 (9)
- July 2007 (9)
- June 2007 (6)
- May 2007 (10)
- April 2007 (11)
- March 2007 (9)
- February 2007 (4)

### Categories

- expository (299)
- tricks (11)

- guest blog (10)
- Mathematics (843)
- math.AC (8)
- math.AG (42)
- math.AP (112)
- math.AT (17)
- math.CA (180)
- math.CO (186)
- math.CT (8)
- math.CV (37)
- math.DG (37)
- math.DS (87)
- math.FA (24)
- math.GM (13)
- math.GN (21)
- math.GR (88)
- math.GT (16)
- math.HO (12)
- math.IT (13)
- math.LO (52)
- math.MG (45)
- math.MP (29)
- math.NA (24)
- math.NT (184)
- math.OA (22)
- math.PR (105)
- math.QA (6)
- math.RA (43)
- math.RT (21)
- math.SG (4)
- math.SP (48)
- math.ST (11)

- non-technical (183)
- admin (46)
- advertising (56)
- diversions (7)
- media (13)
- journals (3)

- obituary (15)

- opinion (34)
- paper (230)
- question (125)
- polymath (85)

- talk (67)
- DLS (20)

- teaching (188)
- 245A – Real analysis (11)
- 245B – Real analysis (21)
- 245C – Real analysis (6)
- 246A – complex analysis (11)
- 246B – complex analysis (5)
- 246C – complex analysis (5)
- 247B – Classical Fourier Analysis (5)
- 254A – analytic prime number theory (19)
- 254A – ergodic theory (18)
- 254A – Hilbert's fifth problem (12)
- 254A – Incompressible fluid equations (5)
- 254A – random matrices (14)
- 254B – expansion in groups (8)
- 254B – Higher order Fourier analysis (9)
- 255B – incompressible Euler equations (2)
- 275A – probability theory (6)
- 285G – poincare conjecture (20)
- Logic reading seminar (8)

- travel (26)

additive combinatorics
approximate groups
arithmetic progressions
Ben Green
Cauchy-Schwarz
Cayley graphs
central limit theorem
Chowla conjecture
compressed sensing
correspondence principle
distributions
divisor function
eigenvalues
Elias Stein
Emmanuel Breuillard
entropy
equidistribution
ergodic theory
Euler equations
exponential sums
finite fields
Fourier transform
Freiman's theorem
Gowers uniformity norm
Gowers uniformity norms
graph theory
Gromov's theorem
GUE
hard analysis
Hilbert's fifth problem
hypergraphs
ICM
incompressible Euler equations
inverse conjecture
Joni Teravainen
Kaisa Matomaki
Kakeya conjecture
Lie algebras
Lie groups
linear algebra
Liouville function
Littlewood-Offord problem
Maksym Radziwill
Mobius function
Navier-Stokes equations
nilpotent groups
nilsequences
nonstandard analysis
parity problem
politics
polymath1
polymath8
Polymath15
polynomial method
polynomials
prime gaps
prime numbers
prime number theorem
random matrices
randomness
Ratner's theorem
regularity lemma
Ricci flow
Riemann zeta function
Schrodinger equation
sieve theory
structure
Szemeredi's theorem
Tamar Ziegler
UCLA
ultrafilters
universality
Van Vu
wave maps
Yitang Zhang

### The Polymath Blog

- Polymath projects 2021 20 February, 2021
- A sort of Polymath on a famous MathOverflow problem 9 June, 2019
- Ten Years of Polymath 3 February, 2019
- Updates and Pictures 19 October, 2018
- Polymath proposal: finding simpler unit distance graphs of chromatic number 5 10 April, 2018
- A new polymath proposal (related to the Riemann Hypothesis) over Tao’s blog 26 January, 2018
- Spontaneous Polymath 14 – A success! 26 January, 2018
- Polymath 13 – a success! 22 August, 2017
- Non-transitive Dice over Gowers’s Blog 15 May, 2017
- Rota’s Basis Conjecture: Polymath 12, post 3 5 May, 2017

## 20 comments

Comments feed for this article

21 October, 2022 at 10:25 pm

AnonymousThe formalization process should be able to detect all the gaps and errors in a claimed proof, and also may help to settle controversies about claimed proofs of important conjectures (e.g. Mochizuki claimed proof of the ABC conjecture)

21 October, 2022 at 10:52 pm

Johan CommelinI do not think that formalization will help to settle controversies that are mostly social, as opposed to disagreement on technical matters. As a thought experiment, suppose a team of formalizers works hard on Mochizuki’s IUTT and gets stuck at the point where plenty other prominent mathematicians got stuck. What will happen? The most likely scenario will be that IUTT-proponents will say: “The proof is nevertheless correct, the formalizers don’t know what they are doing, and they should simply try harder.”

I do not expect that the IUTT camp will suddenly make large efforts to actually explain the proof in detail to people who are genuinely making an effort to understand IUTT. They have had plenty of opportunities to give such explanations, but they don’t seem to want to do that.

22 October, 2022 at 6:48 am

AnonymousThis is only the case if the people claiming to have a proof are not the ones responsible for its formalization.

With a pen and paper proof you can always argue that it’s possible to provide better exposition, or that the verifier is doing some kind of mistake, so there’s no objective standard for what constitutes a complete proof.

With proof assistants we can consider controversial results false until they’re formalized. It wouldn’t be possible to argue that no amount of exposition could convince the verifier without admitting that the argument does not work.

22 October, 2022 at 8:06 am

Johan CommelinThat’s certainly true. You make a valid point. But I don’t think there will be a mathematical culture that requires formalizations of controversial results in the near future. Maybe a few decades from now, but not within 10 years. Of course that’s just my gut feeling.

12 November, 2022 at 9:08 pm

JohnThere will be a mathematical culture to formalize the truly important results, just like there has been a culture to reprove important results using different methods such as elementary ones (PNT) or pure analytic ones (FTA).

22 October, 2022 at 11:14 pm

AnonymousYou say “both communities” in your post. Which two are you referring to?

24 October, 2022 at 11:37 pm

AnonymousThe formalization community (e.g. proof assistant software developers), and pure mathematicians.

23 October, 2022 at 8:12 pm

AnonymousI just realized there is an unpublished Hilbert’s 24th problem

https://en.wikipedia.org/wiki/Hilbert%27s_twenty-fourth_problem

with reference to work of Thiele and Larry Wos which seem relevant to the theme of the workshop ?

24 October, 2022 at 9:13 am

AnonymousWill there be any kind of proceedings published, or online videos of the talks, or anything like that? I’m nowhere near clueful enough to contribute anything as a participant, but am interested enough in the topic to want to find out what happens. There are probably a lot of us out here in that situation. Thanks.

24 October, 2022 at 11:34 am

AnonymousA recent article on some aspects of machine assisted proof is https://arxiv.org/pdf/2207.04779.pdf

24 October, 2022 at 9:48 am

Balasubramanian NarasimhanJust a note to point out that the flyer has the wrong year in the date: February 13-17, 2022!

[I believe this is now fixed – T.]25 October, 2022 at 6:13 am

SouravWill the abstract of the talks be made public before the programme? This may be helpful for those on the fence about registering.

25 October, 2022 at 10:17 am

AnonymousPretty sure the presentations will be on Youtube afterwards.

29 October, 2022 at 11:35 pm

AnonymousDear Prof. Tao, with the registration would it be possible to see the recordings asynchronously (I would be open to register and pay the fee, but I highly doubt I could take part in real time). Best regards, g.

2 November, 2022 at 7:25 am

Allan van HulstFirst of all, thank you for this contribution to formal mathematics and computer-assisted proofs. This is a very important and relevant topic. I am genuinely curious how you look at the following situation.

I recently proved the following theorem in the theory of directed graphs: existence of a kernel implies the existence of a small quasi-kernel in a source-free directed graph (“small” meaning not greater than half of the number of vertices). The proof is here:

https://arxiv.org/abs/2110.00789

I also verified this proof in Coq, just as an additional layer of verification. I then wrote the article in such a way that it resembled the Coq-proof by: (1) writing everything down in a very detailed way, and, (2) referring to the corresponding lemmas in the Coq-proof. This was a bit of an experiment (I was not affiliated with any institution at that point in time, so I had very little to lose).

This paper was rejected by the Electronic Journal in Combinatorics because its style does not “conform to the standards of EJ-C” (per the reviewers) and the Australasian Journal in Combinatorics rejected with similar feedback, after which I gave up and started working on other problems.

My main question at this point: do journals need to re-think what constitutes a ‘good’ proof in the age of formal verification? Or do we researchers need to think of better strategies to get machine-assisted proofs accepted by the wider community? Or perhaps both? Thanks in advance.

4 November, 2022 at 4:33 am

James SmithThese are interesting questions and one I hope they get aired at the workshop.

To me the answer to the second is a combination of controlled natural language, CNL for short, and a TeX-like formal syntax for equations, etc. The combination would be both verifiable and human readable.

See this blog article by Thomas Hales, which overall I heartily agree with:

https://jiggerwit.wordpress.com/2019/06/20/an-argument-for-controlled-natural-languages-in-mathematics/

From my time in academia I recall that there were plenty of journals that accepted formal papers, indeed there was talk of some journals getting to the stage where they accepted nothing else. So you should not give up hope of getting your results published.

7 November, 2022 at 8:21 pm

AnonymousAs you probably know, Chen and Hou recently verified the Hou-Luo blowup scenario for 3D Euler with boundary using a computer assisted proof:

https://arxiv.org/abs/2210.07191

If you are still planning speakers you may want to invite one of them?

11 November, 2022 at 3:40 am

AnonymousI do not need a machine in order to prove that Tao is a moron. This is pretty obvious.

30 November, 2022 at 11:22 pm

AnonymousMaybe by the standards of genetically engineered cyborgs in 2200, but by the standards of modern humans he is pretty smart, and is a reasonable candidate for the smartest human alive.

1 February, 2023 at 2:28 am

Upcoming workshop on “Machine assisted proofs” at IPAM – rosdahal[…] Upcoming workshop on “Machine assisted proofs” at IPAM […]