Intro: Why are Lean and Metamath interesting?
Intro: Why are Lean and Metamath interesting?
From the Project Description: The goal of this project is to do some Metamathematics. The first step will be to work on a Wolfram Language Importer for the Lean Theorem Prover, a currently popular system that blends Interactive and Automated Theorem Proving, two slightly different approaches to finding proofs. Most importantly, Lean draws on the Lean Mathlib collection, made up of thousands of theorems and definitions.
Quick and automated proof checking can help anyone who might like to outsource their proving! Mathematica actually has proving capability and the ProofObject data structure, for equational logic - Lean goes a little further by also allowing quantified terms.
My own way in is that an institute at my university (Research Institute Symbolic Computation at Johannes Kepler University, Linz, Austria) develops a theorem prover that plugs into Mathematica. Bringing in big, community Math theorem packages could be a good way to advance this project. But what is in such a package, how can I explore it? This brings me to Metamathematics and exploring Lean and Mathlib using these approaches.
However, the focus is a prototype for developing the Lean-to-Mathematica bridge, in case other people are interested in this kind of functionality.
However, the focus is a prototype for developing the Lean-to-Mathematica bridge, in case other people are interested in this kind of functionality.
I end on a note about today’s Large Language Models (LLMs) and Neural Networks and how we might plug and play with Metamath, or a metamathematical language, and these new, emergent tools.
Lean-Mathematica Bridge: Setup
Lean-Mathematica Bridge: Setup
The setup part is crucial part of this project: A bridge for Mathematica to talk to Lean (and vice versa) already exists (paper version). As a first step, the WSS project extends (forks) the bridge, to add some convenience functions that can then be used to explore Mathlib, the core, community-driven effort to build a Lean corpus of theorems.
Bridge Setup
Bridge Setup
How does the bridge work? The original repository and the fork including the new functionality are on GitHub, but from the Mathematica point of view, we create a Lean-ProcessObject from the externally downloaded executable (see fork-readme for detailed installation instructions).
In[]:=
LeanExecutable = "lean"
Out[]=
lean
Check/Set the working directory to be mm_lean/src/
In[]:=
Directory[]
Out[]=
C:\Public\WSS2023\mm-lean\src
In[]:=
SetDirectory["C:\\Public\\WSS2023\\mm-lean\\src"]
Out[]=
C:\Public\WSS2023\mm-lean\src
In[]:=
LeanDirectory = "C:\\Public\\WSS2023\\mm-lean\\src"
Out[]=
C:\Public\WSS2023\mm-lean\src
In[]:=
(*Importmain.m*)
In[]:=
<<"main.m";
In[]:=
(*CreateProcessObject*)
In[]:=
Lean=LeanMode[]
Out[]=
ProcessObject
In[]:=
ProcessStatus[Lean]
Out[]=
Running
Mathlib Directory Interface Python Helper-Function
Mathlib Directory Interface Python Helper-Function
For a note on the semantics of the python program being connected to here, see below section “Meta-Mathematical Explorations of Lean.” (There is a caveat.)
Python was chosen after a brief performance test in comparison to TextSearch[](* //RepeatedTiming *) in particular.
To make sure Python is installed and found by Mathematica: FindExternalEvaluators[“Python”] on your system.
To make sure Python is installed and found by Mathematica: FindExternalEvaluators[“Python”] on your system.
In[]:=
MathlibDirectory = "C:\\Public\\WSS2023\\mathlib\\src"
Out[]=
C:\Public\WSS2023\mathlib\src
In[]:=
session = StartExternalSession["Python"]
Out[]=
ExternalSessionObject
In[]:=
TheoremMarker = "(theorem|lemma)" (* Particular to current Lean/Mathlib syntax, see caveat *)
Out[]=
(theorem|lemma)
In[]:=
ExternalEvaluate[session, File[LeanDirectory <>"\\directory_interface.py"]] (* See GitHub *)
In[]:=
MathlibTheoremOccurrencesByDomain[domain_] := {domain , ExternalEvaluate[session, <|"Command"->"count_occurrences","Arguments"->{MathlibDirectory <> "\\" <> domain,TheoremMarker}|>] }
In[]:=
MathlibDomains = {"algebra","algebraic_geometry","analysis","category_theory","combinatorics","computability","control","data","dynamics","geometry","init","logic","meta","number_theory","order","set_theory","system","tactic","topology"}
Out[]=
{algebra,algebraic_geometry,analysis,category_theory,combinatorics,computability,control,data,dynamics,geometry,init,logic,meta,number_theory,order,set_theory,system,tactic,topology}
The above are the domains we will be interested in for the context of this post.
Lean-Mathematica Bridge: Adding to the Bridge
Lean-Mathematica Bridge: Adding to the Bridge
A quick note on what we are actually doing to begin: we are interfacing with the Lean executable. Under the hood, when call get our additional info about our Lean proof for instance:
In[]:=
GetLeanInfo[p_ProcessObject, name_String] := Module[{res, content}, content = StringForm["import main imports set_option pp.beta true open tactic.interactive #view_info ``", name]; SendToLeanServer[p, content // ToString]; res = HandleLeanServerResponse[p]; ("text" /. res[[1]]) // ToExpression];
Getting a (visual, grid) representation works much in the same way: this leads me to finding a way to interpret a proof like this in Mathematica.
getLeanTree[] to Get a Handle on the Theorems (Make Them Computable)
getLeanTree[] to Get a Handle on the Theorems (Make Them Computable)
The main improvement I think I can add to the current bridge is a computable data structure that is also more compact in some ways. Take the following proof grid box as an example:
In[]:=
leanProof=GetLeanProof[Lean,"nat.prime.dvd_of_dvd_pow"]
Out[]=
Goal | ∀ {p m n : ℕ}, nat.prime p → p ∣ m ^ n → p ∣ m |
ID | 24 |
Rule | ∀I |
Proofs |
Lean is not so much the focus of study here, but this the corresponding Lean code:
theorem prime . dvd_of _dvd _pow {p m n : ℕ} (pp : prime p) (h : p ∣ m^n) : p ∣ m :=
begin
induction n with n IH,
{ exact pp . not_dvd _one . elim h },
{ rw pow_succ at h, exact (pp . dvd_mul .1 h) . elim id IH }
end
begin
induction n with n IH,
{ exact pp . not_dvd _one . elim h },
{ rw pow_succ at h, exact (pp . dvd_mul .1 h) . elim id IH }
end
The statement can be seen as a lemma in number theory. It means that if a prime number p divides m^n (where n is a natural number), then p must divide m.
We can write this as a function too, but it is not a proof, just an application of the theorem (lemma).
In[]:=
PrimeDivisorProp[p_,m_,n_]:=PrimeQ[p]&&Divisible[m^n,p]->Divisible[m,p]
In this function PrimeDivisorProp, we first check if p is prime with PrimeQ[p], then check if p divides m^n with Divisible[m^n, p], and finally we check if p divides m with Divisible[m, p]. The -> operator represents logical implication in Mathematica, which matches the structure of the statement. But again, while this function will correctly express the logical statement, it does not actually prove the statement.
So let’s switch to the Lean bridge: For us it is important to understand that there is some sense in which these proofs unfold from a set of axioms. The project being built on (see introduction) hands out IDs for the individual proof steps.
From the integer ID we can tell that there are 24 theorems involved: this number will come back later.
But: Even at this size, which could conceivably be a lot bigger, trying to analyse the proof structure quickly becomes unwieldy ...
But: Even at this size, which could conceivably be a lot bigger, trying to analyse the proof structure quickly becomes unwieldy ...
A more compact version in the form of a tree structure makes sense, but the built in option still has too much information and is not computable, although the structure is more compact and apparent.
In[]:=
leanProof//TreeForm(*Thisworksquitewellinsomebutnotallregards*)
Out[]//TreeForm=
So here is a function to simplify to a tree, building on this initial proof representation: The thinking is, this kind of positional structure being interpreted here is liable to be found on some level, although maybe there are better Lean commands to interpret the output of. This shall serve as an initial exploration in this direction, in case this might be something worth further building on.
We might also like to flip the tree to the left:
This current iteration maps to the IDs relative to the proof that is being worked out by Lean, but we could also just get Lean syntax representations, or any of the Lean output we are interested in.
The point is that the structure is the proof goal on top, the logical proof steps to get there (proof combinations), starting from the axioms in the leaves. We might want to isolate these, by the way, to see what our basic assumptions (per proof) are.
Or, in case we are just interested in the amount of axioms used, not the structure:
Let’s move towards more metrics and aways from structure.
Summary Statistics, or a Metamathematical Language for Proofs?
Summary Statistics, or a Metamathematical Language for Proofs?
What the tree representation allows us to do now are simple tree algorithms to get summary statistics concerning the proof set and especially structure of the proof.
We can use the proof grid the original project intended and don’t even need to know about the trees, from the user’s point of view.
Metamathematically interesting to note here: the size of our tree is larger than the largest ID (this is why it makes sense to look at the tree in terms of IDs as well). This is because certain theorems are re-used, so individually there are 24 theorems, but we apply them 30 times. One can think up a utility functions, or better a metric, that might tell us about re-use of theorems, or the re-used theorems.
In this line of thinking: a higher metric would point towards a more repetitive, perhaps more “boring,” proof.
Another simple one: How deep does our tree go?
Which might tell us something about how “difficult,” because of all the steps that occur, or just “deep”, or “involved,” a proof is.
The focus here has been Lean-Mathematica interoperability and ease of use, by abstracting over the trees which were chosen as the appropriate data structure in the background. Efficiencies might be discovered in that the tree might be easier to construct another way (using more appropriate Lean input), but the idea is to use the tree in the background and keep the original developer’s intentions for proof representations intact. The user needn’t even know about the tree conversion going on in the background.
To make a point about the actual doing of Metamathematics: This is a different approach “under the hood” compared to the directory/web scraping approaches taken in the following, since we are conversing directly with the lean package installed in our system. In the following we will analyse the Mathlib library we specified in setup.
To make a point about the actual doing of Metamathematics: This is a different approach “under the hood” compared to the directory/web scraping approaches taken in the following, since we are conversing directly with the lean package installed in our system. In the following we will analyse the Mathlib library we specified in setup.
Meta-Mathematical Explorations of Lean
Meta-Mathematical Explorations of Lean
We continue our exploration on another level, that of our corpus of all proofs, not individual ones (in terms of other proofs and axioms).
We also make use of a different data structure under the hood: a graph.
We also make use of a different data structure under the hood: a graph.
Zoom out: MathLib, Where are We at in 2023?
Zoom out: MathLib, Where are We at in 2023?
We have the notion of mathematics as a universal language but we can see here that there is also a body of knowledge (developed by a community) involved. For anyone who might be interested in exploring the metamathematical space: How has this body of knowledge evolved in the past three years, say, and might this indicate something about future development?
The first part to answer this question is from 2020, where I draw on the Euclid article by Stephen Wolfram and others - the focus here was interconnection.
The above emphasizes dependencies and connections, but here we will make our historical comparison simply based on size:
Compare to 2023
Compare to 2023
I want to look at how Mathlib is evolving, particularly what domains are growing the most: We can do this, by “simply” (see caveat below) looking at the structure of the relevant GitHub repository in its current state (July 2023).
Let’s do some more visualizations, but notice some Lean infrastructure categories we do not care so much about.
Notice also that the lists are not completely congruent.
After having cleaned the data in this way we are ready to study the development of Mathlib along these lines.
But is this feasible, one might ask: by directory-categorization, some areas are shrinking and some areas are growing, so much so that the data schemes might be off.
Another representation shows the overall corpus distribution for 2020 and 2023 using these schemes more clearly.
Another representation shows the overall corpus distribution for 2020 and 2023 using these schemes more clearly.
We might conclude from these observations that directory scraping is problematic, so let’s observe the following caveat.
Caveat
Caveat
This data comes about through web/directory scraping, some time around 2020 when the article was published. But Mathlib evolves and in fact is becoming very big. Asking about this in the Lean Zulip forum, Scott Morrison, one of the programmers and mathematicians working on Lean, responds: “Overall, I would say Mathlib is already too big to “get a sense of all the theorems” in any meaningful [way]! I’m sure every expert here is regularly surprised to find that something is, or is not, in the library. (Within specific areas this is not true.)” And: “The directory structure in Mathlib is fairly ad-hoc and to a large extent based on historical accident, so be very skeptical of any ‘overview’ based on analyzing file names or namespaces!”
Maybe we can at least make some overall statement about the growth trend of Mathlib, so let’s conclude with the following summary overview of this line of inquiry.
Zoom Back In: Theorems Crossing Domains, More Metamathematical Language for Theorems
Zoom Back In: Theorems Crossing Domains, More Metamathematical Language for Theorems
Back on the level of individual theorems we might like to make visible the area of mathematics they originate from and how they can come together for different kinds of proofs. (This shows one way different levels of abstraction in metamathematics can work.) This may again allow us to articulate metamathematical statements about proofs, perhaps saying something about how “surprising,” or “encompassing” a given proof is. The point of departure for these second types of descriptors for proofs is their relation to other proofs in a network of proofs. Crossing domains might also require interpretation of analogous proofs across domains. More such descriptors were also developed in A New Kind of Science.
Possible Broader Implications
Possible Broader Implications
As a side-note about potential implications, with LLMs recent rise to prominence, this kind of metamathematical language (word choices) as well as metamathematical programming languages like Lean might be particularly fruitful. One can imagine Neural Networks exploring these metamathematical theorem spaces in ways approaching how humans do mathematics: But I defer to Stephen Wolfram on the details of the broader implications and this line of thinking, outside of the scope of this project, which focused on prototyping possible infrastructure.
Thanks
Thanks
I would like to thank the following people for their inputs throughout Wolfram Summer School (WSS) 2023 along with all the Wolfram staff for making this school a great time and excellent way to learn Mathematica: Mark Greenberg for help on the visuals (he has wonderful taste) and, together with Christopher Wolfram, especially help on the proof-to-tree transformation; my WSS-mentor Eric James Parfitt for excellent guidance; Swastik Banerjee for exploring the Python interoperability part; Mano Namuduri and Nik Murzin for input and help from the perspective of the original Euclid article.
CITE THIS NOTEBOOK
CITE THIS NOTEBOOK
Empirical metamathematics: extending the Lean-to-Mathematica bridge
by Jack Heseltine
Wolfram Community, STAFF PICKS, July 11, 2023
https://community.wolfram.com/groups/-/m/t/2957419
by Jack Heseltine
Wolfram Community, STAFF PICKS, July 11, 2023
https://community.wolfram.com/groups/-/m/t/2957419