In an age of proof abundance, what becomes scarce?

In his talk, The Future of Mathematics, Dr. Kevin Buzzard states that Lean is the only existing proof assistant suitable for formalizing all of math. In the Q&A part of the talk (at 1:00:00) he

LLMs have turned a corner — from solving textbook problems to scoring top marks at the world's hardest math contests and cracking unsolved conjectures, all with minimal human oversight. How did we get here, and what does the current landscape of AI-powered formal mathematics look like?

How AI could destroy mathematics and barely touch it

The inside story of Lean, a computer program that answers the age-old question: How do you know if something is true?

I formalised and proved the correctness of Move’s new borrow checker in Lean: 39,000 lines of mechanised metatheory, produced in under a month with the help of an AI coding assistant. This post tells the story of how it went and what it means for the future of PL research.

I am a computer scientist.

Leonardo de Moura — Creator of Lean and Z3

Presentation by Adam Pease at SRI, Menlo Park, CA. I discuss implementation details of writing an automated theorem prover in Java for first order logic. A su...

People expect perfection. Consider the reaction when someone who has been vaccinated against a particular disease nevertheless dies of it.

There used to exist a "top 100" of mathematical theorems on the web, which is a rather arbitrary list (and most of the theorems seem rather elementary), but still is nice to look at.

Since the release of my preprint with Tim, Ben, and Freddie proving the Polynomial Freiman-Ruzsa (PFR) conjecture over $latex {\mathbb F}_2$, I (together with Yael Dillies and Bhavik Mehta) have st…

Contribute to JOSHCLUNE/LeanHammer development by creating an account on GitHub.

This repository contains various json files indexing sorries in public Lean 4 repositories. They are generated using the crawler developed in the SorryDB project.

the quick and dirty of Lean

Live demonstration of the Lean interactive theorem prover, showing how formal logic rules are encoded, manipulated, and verified, and discussing its role in mat...

Continuous functions play a crucial role in various disciplines in math. We discuss the epsilon-delta criterion and formalize it in the programming language and...

In this experiment, I took a statement in universal algebra that a collaborator of mine (Bruno Le Floch) on the Equational Theories Project had written a one-pa...

Following on from the previous video at https://www.youtube.com/watch?v=cyyR7j2ChCI, I now attempt to formalize a different proof of the same assertion using th...

—————SOURCES———————————————————————— Percolation – Béla Bollobás and Oliver Riordan Cambridge University Press, New York, 2006. Sixty Years of Percolation – Hugo Duminil-Copin https://www.ihes.fr/~duminil/publi/2018ICM.pdf Percolation – Geoffrey Grimmett volume 321 of Grundlehren der Mathematischen Wissenschaften [Fundamental Principles of Mathematical Sciences]. Springer-Verlag, Berlin, second edition, 1999. —————NOTES————————————————————————— Note at 10:42 – The uniqueness of the infinite cluster is known for the d-dimenional lattice since the works of Aizenman, Kesten and Newman - [Uniqueness of the infinite cluster and continuity of connectivity functions for short and long range percolation (1987)] and Burton and Keane - [Density and uniqueness in percolation (1989)]. It does not hold in general: when the graph in question is a regular tree for example, there are always infinitely many clusters during the supercritical phase. The two last results shown here are only known for site percolation (in which vertices are open or closed instead of edges) in the triangular lattice, where a scaling limit for the boundaries of critical clusters was proved to exist (more on that in the third note). It is believed that these results are universal, that is, valid in great generality for planar percolation processes near criticality. The third result is from an appendix by Gábor Pete in the paper [Scaling limits for the threshold window: When does a monotone Boolean function flip its outcome? (2017)] by Ahlberg and Steif. Consider an n by n box, and the event where there exists a left-right crossing of said box. Recall the uniform coupling from the video: intuitively, the result is saying that the point at which this crossing emerges in the uniform coupling is with high probability inside an interval of size n^{-3/4} around 1/2. The fourth result is saying that the average size of the cluster of the origin (or any other given point) goes to infinity as we let p approach the critical parameter like a specific power of the distance between p and p_c. This power is called a critical exponent. The existence of these exponents was proved by Smirnov and Werner in the paper [Critical exponents for two-dimensional percolation (2001)]. Note at 10:52 – Hugo Duminil-Copin has several major contributions to the study of processes arising in statistical physics, including Bernoulli percolation. Among his works on Ising and Ising-like processes we can cite [Random Currents and Continuity of Ising Model’s Spontaneous Magnetization (2015)] with Aizenman and Sidoravicius and [Sharp phase transition for the random-cluster and Potts models via decision trees (2019)] with Raoufi and Tassion. Note at 12:38 – In the triangular lattice site percolation, Stanislav Smirnov proved the conformal invariance of crossing probabilities at criticality (see https://www.unige.ch/~smirnov/papers/icmp-final.pdf for an overview), which led to the proof of the existence of scaling limits of exploration curves as Schramm–Loewner evolution processes. See [Critical percolation in the plane (2009)] by Smirnov. This provided a deep understanding of the critical phase in the triangular lattice site percolation, which to this day is not extended to the square lattice. Note at 17:52 – It is not at all obvious that the probability of being connected to infinity is continuous above criticality. This result can be proved in the d-dimenional hypercubic lattices using the uniqueness of the infinite cluster, and more generally it was proved for transitive graphs (intuitively, graphs in which all vertices look the same) by Häggström, Peres and Schonmann in [Percolation on transitive graphs as a coalescent process: Relentless merging followed by simultaneous uniqueness (1999)]. —————SECTIONS——————————————————————— 0:00 Introduction 1:37 Definition – Bernoulli Percolation 5:23 Definition – Uniform Coupling 7:56 Exploration – High-Resolution Square Grid 9:40 Exploration – Questions and Kesten's Theorem 10:58 Exploration – Ising Model 11:54 Exploration – Critical Percolation 12:50 Exploration – Three-Dimensional Cubic Lattice and Beyond 14:13 Proof – Theorem Statement 15:14 Proof – Simplifications 16:29 Proof – Definition of Critical Parameter 18:41 Proof – Critical Parameter is Greater Than Zero 20:44 Proof – Duality Definition 21:56 Proof – Critical Parameter is Less Than One 25:16 Proof – Summary and Idea for Kesten's Theorem 26:11 Conclusion —————CREDITS———————————————————————— Caio Alves – writing, 3D animation Aranka Hrušková – writing, clarinet Vilas Winstein – writing, 2D animation, editing, voice-over Special thanks to Anisah Awad, Gábor Pete, Jyotsna Sreenivasan, Angie Zavala This video is an entry in the second Summer of Mathematics Exposition (#SoME2) The photographs used in this video are licensed under the Creative Commons Attribution-ShareAlike license: https://creativecommons.org/licenses/by-sa/4.0/deed.en Uploader: Spectral Collective Duration: 1612s Views: 455517

Note: this post was written for Lean 3; the latest version, Lean 4, is a very different language. Turn back the clock to 2009: a confused physics major newly infatuated with math and computer science, I enrolled in MATH 273: Numbers and Proofs at the University of Calgary. This wasn’t my first encounter with mathematical proof; in first-year calculus I’d mastered rote regurgitation of delta-epsilon proofs. Despite writing out several dozen, their meaning never progressed beyond a sort of incantation I can summon to this day (for every \( \epsilon > 0 \) there exists a \( \delta > 0 \) such that…).

While conceptually simple, this feature actually requires more engineering effort than one would expect - in particular, tracking the set of known malicious URLs in a practical manner turns out to be somewhat difficult.