How to Formalize All of Mathematics | Hacker News Reader

How to Formalize All of Mathematics

xenaproject.wordpress.com

98 pointspractal87 comments

Reminds me of the following papers (from 1979!) by Ernst Snapper;

1) What is Mathematics? - https://sci-hub.reatk.com/10.2307/2320582

2) The Three Crises in Mathematics: Logicism, Intuitionism and Formalism - https://sci-hub.reatk.com/10.2307/2689412

AI is the fourth crisis in Mathematics!

Formalism has been so successful that the General Public thinks that is all there is to Mathematics. And now AI has made this trivial.

But hopefully, Mathematicians are looking at more foundational and philosophical underpinnings.

The thing is that logicism and formalism were both essentially successful - Godel might thrown a wrench into Hilbert's plans but correcting for the incompleteness problem, a formal process can go forward. Intuitionism was a failure in the sense that just the existence of computers shows

The thing is, I think mathematics as a whole has reached a bit of the sort of crisis that mathematical foundations reached after Godel's theorem. I think Raymond Smullyan said something like (paraphrasing)"We know the continuum hypothesis is independent, it can't be proven or disproven by other hypotheses, we're not trying to do that. But if it can be stated in such a way that it is as intuitively clear as the other other axioms of set theory, then it will likely be accepted".

Mathematicians now can cruise through a huge area of "what can be mechanically deduced/mechanically constructed" and it seems like the task becomes highlighting what matters to us (as humans or mathematicians or some community) within that realm.

Intuitionism And constructivism is fundamentally how computers function.

> “But if it can be stated in such a way that it is as intuitively clear as the other other axioms of set theory, then it will likely be accepted"

The internal/external logic of sets is exactly where Set gets confusing with computation.

Subsingletons (mere props) being choice theoretic is exactly where we have to resort to HoTT etc..

That shift in limitations from internal vs. external is a lens on many independence results.

> Intuitionism was a failure

Not true; Eg. Intuitionism via Constructivist Mathematics gave rise to Intuitionistic Type Theory and its various derivatives which are all fundamental to doing "correct" computation.

By forcing one to come up with "proof of existence" by constructing it, in a way, it is more fundamental than Classical Logicism where truths of certain propositions on certain structures are accepted a priori. But once Intuitionism itself was formalized, people forgot its philosophical underpinnings leading to our lack of understanding today.

See also my other comment here - https://news.ycombinator.com/item?id=50127948

The current cycle of AI and mathematics gives me great hope for ordinary people like myself to try and attempt learning some mathematics and try and see if I like the experience. Has any one tried that or is trying that? How are you approaching it? I would like to know - you can DM me - I would love to have a conversation if this excites you :)

I think the _key_ to knowing if I can do it has to come from the fact if my intuition about a problem helps me make progress. I would use AI to learn the parts I did not know and engage a community of people to ask questions. Both are key.

Also I am not 100% sure, but me beginning straightaway with lean to try something — like an engineer would — does not seem like the right approach before building some critical mass in the subject. It feels kinda wrong like building the cart before the wheel would.

I can chime in about this. I’m a software engineer and about 7 years ago I decided to get a masters in pure mathematics. Because I was working full time, I could not attend any class so I self studied from textbooks and it worked well.

When I would get stuck, I would struggle with the problem, ask around, ask on Math Stackexchange and along the process I would end up learning a lot more.

With AI now, it’s like having your own tutor: you can ask personalized questions and it would answer it very well.

But that would also mean the amount of time I would spend struggling would go down considerably.

So you really have to be self disciplined and struggle with the problem a little bit before asking for help. You can also ask it to give hints only.

Do not mistake understanding the answer with learning something rigorously.

So if you are curious and doing an exposition, use it as you would normally and it will work wonderfully.

But if you want to learn it rigorously, our usual present habits with AI spitting out answers and us reading them will not work at all.

I wonder: can you get the AI to give you exercises that, when solved, would illustrate a point? This might require more theory of mind than they have.

I've tried to do this but with learning poker, and it's sort of a mixed bag. You kind of have to know what you don't know before you can get anything useful out of it. It can sort of help going from "I understand this concept, but not instinctively" to "I've drilled this enough that I could do things like this in my sleep", but it takes a lot of iteration and asking questions before it can settle on a series of instructive examples that each build on top of each other. You're still much better off with a well-written textbook.

The problem with trusting AI to learn a complex subject, which I've tried multiple times, is it will always at some point confidently give you the wrong explanation for something important and you will have no way to detect it. Its quite frustrating and that realization might not come for hours or days and you've built lots of false mental models that can be hard to untangle.

You have to do it along with some sort of ground truth, like a book, and you have to be able to understand that book in order to be able to see that bad advice immediately.

Alas, there are no shortcuts in life. You still need to very eagerly read and understand the source materials you're studying as you would have before AI and to the extent which AI is helpful for that is debatable. Your brain still has to do the thinking.

I agree with the sentiment of mixing up sources. However there are not really many textbooks that rise to the level of "ground truth". Plenty of times that books give wrong explanations as well.

Well I said sort of, but I'd argue most significant works in significant fields do not give completely incorrect explanations, and if they do there's usually versions of those works and they are updated. Your llm conversation is not versioned, there is no consensus built around its correctness.

In my experience learning with llms is the equivalent of doing (bad) tutorials, and you end up in tutorial hell where you feel like you're learning but you find it hard to implement said thing without that guide. It creates surface understanding thats not really worth the effort. Its better to dive deep on your own.

We're all looking for that shortcut, myself included, but as the saying goes, "there's no free lunch".

So... use a RAG trained on the books you care about?

>The problem with trusting AI to learn a complex subject, which I've tried multiple times, is it will always at some point confidently give you the wrong explanation for something important and you will have no way to detect it. Its quite frustrating and that realization might not come for hours or days and you've built lots of false mental models that can be hard to untangle.

This is an amazing problem to have! Often, preAI, I'd reject models flat out since they weren't even convincing on their face. There is value to this even if it's not correct. How long were people stuck with the aether? a few days or months is nothing.

I would think the exact opposite. I always lacked academic rigor and I own that.

How could you come in with less rigor and claim to understand things because you're using AI?. Sorry for the aggressive tone but is there an answer to that questipn?

In my experience AI is a very bad teacher. It mumbles in AI-ish, a dialect of English which is difficult to understand without reading things twice. Also, it uses concepts before they are defined. And doesn't have a good mental model of what the reader knows. Stuff like that.

AI labs definitely should work on it.

I think AI is more effective as a tutor than as a teacher. The student sets the curriculum and does the work up front (e.g. writing up LaTeX notes) then the AI checks it and answers questions with the notes as context. I've had some success with this approach for theoretical physics, but it is clunky and maybe there's a better solution.

> - you can DM me -

...how?

HN profile.

Claude Code will make Bartosz Ciechanowski-style [0] explainers for me in about 3 or 4 hours. Here is an example of converting waveforms into spectrograms to train a model to associate sounds with words or classifications. [1] Or, it will take the research paper for Data Lake and convert it into animated, step-by-step visualizations explaining how the data store works. [2]

It is still work! And, I have to struggle to get it to make sense and look nice. This means I'm interacting with the code and system which is how I learn!

[0] https://ciechanow.ski/sound/

[1] https://adamsohn.com/clap/

[2] https://adamsohn.com/algoviz/?algo=delta-week

If you want to learn a mathematical topic, I would recommend reading textbooks instead. They are expressly designed for the purpose by experts on the topic.

"Reading" a textbook is very different from reading a novel, that should be noted. You gotta do the exercises.

I might suggest also trying to find online a syllabus for a course that taught that topic using that textbook. That can give you an idea of a reasonable pace to learn the material. If you can't find one using the same book, you still can get some idea of pacing based on the topics listed.

A good textbook will be designed so that you can move on when when you just have a decent understanding, and your understanding will deepen and complete as you gain experience from the material being used to help teach the new material in later chapters.

At the point where it is OK to move on most students feel like they are nowhere near ready. If you just move on when you feel ready it is easy to find yourself a few months later wondering why it has taken you several months to get to chapter 3 when you know that in college students finish the whole book in that amount of time, which taking several other classes.

It is OK if you go slower than the college classes. If you can't put in as much time per week as college students do you would be expected to go slower. Just use the college pace, adjusted for how much time you can put in, to help know when it is OK to move on so you don't get stuck due to thinking you aren't ready.

It can also help if you can find a list of assignments for a class that used the same book. That can give you an idea of a minimum number of exercises you should be doing. It is ok course OK to do more.

For many STEM subjects, MIT OpenCouseWare [1] is a good place to find syllabi and often much more for free.

[1] https://ocw.mit.edu/

Use a good (human-written) textbook and solve the exercises. Use AI to ask clarifying questions when necessary.

After all that spam on Tao's blog, I'm honestly kinda tired of "guest posts"

I track blogs because I'm interested in a specific person. I feel disconnect with different style, narration and naming of the new author

Just... make a new blog for new person and start linking posts to each other. C'mon

IMO mathematics benefits from being highly generic compared to normal code, so much so that the implementation itself doesn't really matter (and it's entirely normal in mathematics to skip details, unlike in software). So then to me it makes sense to have a clean separation between basically header files and implementation files like in C and C++. Then something like mathlib should be a pristine collection of what belongs in headers: data structure definitions, instances, theorem statements, macros/tactics for common techniques, etc. So basically it is a curated set of "axioms" that can be used for other math and remain understandable, indexable, etc. Maybe a companion mathlib-full that can actually compile the entire theory.

I suppose this could be done with just tooling to generate a skeleton/index of a giant repository of all mathematics if you decided that you're going to index all definitions and theorems but not lemmas or examples or something like that.

Indeed, what I'd like is formal mathematics proving language that could be viewed as an outline in that natural language math proofs are structured as outlines. The reader would be able to choose what to view - definitions, theorems, lemmas, examples, key-steps, all steps etc.

Ideally, a view would let a reader expand into not just the proof at hand but the various theories in the repository.

A reader could even tell their viewing preferences and it might strip down the UI for those purposes.

Yes, I had similar thoughts last week: https://news.ycombinator.com/item?id=49995658

> proper IDE for math

Love this concept, and the potential for a far more integrated interface with various features that smartly supports the author, like a structural/projectional editor with built-in understanding of mathematics.

That makes me imagine a future where various languages import their core data structures and algorithms from a common, language-agnostic "standard library" of mathematically rigorous foundation.

Math is not about the definitions. It is about the connections between these definitions. And the techniques used to establish broader classes of connections between similar objects.

The way we formalize a connection is with a proof. And if the proof is "nice and modular" it sorta explains by itself how it can be used for similar problems.

And such proofs definitely belong into MathLib. There is often value in actually reading the Lean proof script (especially with the IDE support like jump to definition). It is not only there for the machine.

Lemma, Theorem, Proof, Repeat.

Proofs are not nice and modular though unless they can be extracted into a macro/tactic (or theorem), which I said belongs. They are literally not reusable. The perspective I'm coming from is that we should extract what is valuable as elevated theorems, leaving only the not-so-valuable technical details as the proofs. The connections between objects are theorems.

Hasn’t this been tried already?

You might be thinking of the Langlands program

You give me too much credit. I was just being tongue-in-cheek about Principia Mathematica.

The Langlands program is about correspondences between analytic number theory and harmonic analysis. You could think about it as a unification of parts of mathematics that seem to have no reason to join up but turn out to have deep and non-obvious connections. It doesn't have anything to do with formalization.

Here's a really good and accessible intro to Langlands https://www.youtube.com/watch?v=4dyytPboqvE

I thought Stephen Wolfram had already done some victory laps.

Formally verifying all of math would be an amazing achievement by humanity.

V.I. Arnol'd: "Only fools prove theorems."

(The wording may not be exact, though the sense should be.)

Do you think this silly comment is somehow profound? Math is mainly about proving theorems true or false or finding counterexamples.

And nevertheless this is what Arnol'd said. Do you also think he was silly?

Yes that is an extremely stupid thing for a mathematican to say and pointless to quote.

I like the pragmatic take on AI in mathematics. Running off and proving/formalizing things in incomprehensible ways is marginally useful, and probably harmful for any work that needs to move beyond it. But, there's value in what AI is capable of doing for working mathematicians, when used as a partner.

The genie is out of the bottle though. It's hard to see how there won't be weird and inscrutable branches of mathematics that LLMs build and use effectively _for themselves_, in the same way much of the slop LLMs write in spoken language is really for the consumption of LLMs.

Surely there will be a new kind of research mathematician that's investigating this output in the same way, say, academics in literature read.

> in the same way much of the slop LLMs write in spoken language is really for the consumption of LLMs.

Is it though? We're not benchmarking how well LLMs 'like' it, and slop is characterised by an unnatural absence of useful information.

It seems mostly designed to mislead humans into believing it was written by someone knowledgeable on the subject.

We research mathematicians are still learning how to use AI in research and how to deal with the output. I drafted eight papers last weekend. This week I advanced on none. AI still gets stuck at the key point on a problem where there isn't already a lot of work done. What falls is where techniques not known to the researcher are available and profitably employed - ai brings them into the fray fast - and someone with experience immediately sees where to go with it - and the dominos fall.

So far AI still doesn't make definitions. It tries but it doesn't really see structure - only patterns on which it can impose (by brute force) known structures.

What's not clear is how the professional infrastructure will survive. Journals seem likely to die. The arxiv is swamped. A human can't assess the volume of the output. Serious conjectures have fallen and serious people have checked them.

We are looking for constructive and productive and socially useful ways forward. One reflection is that a lot of what we have been doing was maybe not so interesting as we thought.

Only a minor in mathematics here. That's interesting that it struggles with definitions. Maybe unsurprising given the different ways they're chosen and written (motivational, aesthetic, pedagogical, etc)? A big lever to keep hold of.

> where techniques not known to the researcher are available and profitably employed - ai brings them into the fray fast - and someone with experience immediately sees where to go with it

> So far AI still doesn't make definitions. It tries but it doesn't really see structure - only patterns on which it can impose (by brute force) known structures.

Insightful and nicely phrased!

Mathematicians are victims of their own success, by systematizing Formalism which made AI possible in the first place.

Paradoxically, they should also be indicted for removing the Human element by deemphasizing the study of Philosophy of Mathematics (i.e. ontology/epistemology/discovery/invention) and its mapping to Reality, but focusing only on formalization as an end in itself.

As you point out, the "definitions" (i.e. conceptual theory) are what is the critical aspect of discovering/inventing/doing mathematics and this has been forgotten in mathematics education since the Formalists gained ascendancy.

I think it is time to go back to the foundations of Mathematics and its Teaching viz. various types of Logical Reasoning, discovered/invented structures and their relationships based on Reality (the ontology and epistemology), with the final goal of understanding Nature itself.

$ChatGPT> "How to Formalize All of Mathematics?"

AI has all the answers. Why read the article?

Title isn't true. It is a subset but clickbait gotta clickbait.

Did you read TFA? They never claimed they’ve formalized all of mathematics. For a couple decades now, mathematicians have been discussing formalizing all of mathematics. Some are now proposing AI can be used for this. But TFA argues that’s not necessarily the best approach. It’s a discussion of how to move forward in formalizing all of math, not a claim about having done so. Not clickbait at all.

I didn't claim that they claimed to have done it. My point is that you cannot do it.

You cannot formalize ALL of mathematics. We have known that for a while. Hence my point about the title being clickbait.

At best that seems like a nitpick based on a specific notion of “all of mathematics”. Care to explain what you mean?

The title is intentionally misleading because the authors know all of mathematics is not possible to formalize, strictly speaking. And strict meaning is what math is all about.

Would you have been happier if we had called it "...all known mathematics"? This is what we are plainly talking about. The question we attempt to address is how best to digitise the corpus of known mathematics.

Would still have been wrong.

Godel would like to talk to you about his “Incompleteness Theorem”

Also Chaitin would like a few words.

The Limits of Mathematics: A Course on Information Theory and Limits of Formal Reasoning - Chaitin, Gregory

https://ia801804.us.archive.org/35/items/A-Z_Library_G-K_Jos... (PDF)

Yeah which is why I don't have much sympathy for folks like Tao either

The ability to conjure math is practically as endless as time

At some point the outcome is just generation of new visual art in the form of syntax

We can't physically observe the past or future so we can only theorize and simulate; IMO that's the physical phenomena that belies Incompleteness Theorem; from Earth in the relative year of 2026 my view of the universe is fundamentally incomplete. As such all language describing too far either is incomplete always.

It makes any kind of longtermism, religious or agnostic framework espoused by kids of rich academics, empty. We all gonna stick around 10 more generations just to make sure?

Whole lot of educated people are just peddling euphemism for religious conviction they steeped in as kids but hid behind atheist semantics like "Intelligent Design."

This is irrelevant. The theorems Avigard, Buzzard, et al. are talking about all have natural language proofs already that in theory should be formalizable.

They are not claiming all possible theorems are formalizable. They are claiming to try to formalize all already proven theorems in the mathematics canon.

To the extent the theorems in question are impossible to formalize this means the original proof must be in error.

Then, "All of Mathematics" is being used as clickbait.

I pretty strongly disagree. The body of the text was what I expected based off the title.

The article is not meant just for you.

>To the extent the theorems in question are impossible to formalize this means the original proof must be in error.

Theorems by definition must be formalizable. A theorem is not simply a true proposition, it's a provable proposition and a proof is necessarily a formal/syntactic property of a proposition.

That said, I agree with the sentiment that dismissing the entire article on the basis of the incompleteness theorems is shallow and the article is not about formalizing "all" of mathematics in the strict sense. It's mostly about introducing formal tools to the everyday mathematics.

> Theorems by definition must be formalizable. A theorem is not simply a true proposition, it's a provable proposition and a proof is necessarily a formal/syntactic property of a proposition.

Yes that's fair. To be accurate the formal definition of a theorem entails that provability. I was being too loose in essentially using "theorem" to refer to any proposition.

If a theorem has a published proof, it is either formalizable or incorrect.

No. This is not how this works.

As the silliest example of this: the Calculus of Inductive Constructions (the core calculus implemented in Lean) has a published proof of its soundness (that you cannot derive False in it). That proof can (probably, thanks to Gödel) not be formalized in Lean or any formal system of axioms weaker than Lean.

If what you were trying to do was define what it means for something to be a correct proof, then you must equally admit that there can't be a correct proof of the fact that Lean can't prove False. And if you find that world a happy world to live in while we delegate all concerns about truth to Lean, then I have an infinite hierarchy of monotonically growing bridges to sell you.

Yes. This is how this works.

Any proof which is correct can be formalized. That is what is means for a proof to be correct.

I’m not sure why you are restricting the scope of our discussion to what _Lean_ can(not) formalize. Even if we do choose to do that for some reason, Lean is not a formal system of fixed axioms; it supports optional additional axioms.

In principle, a computer can check a nonconstructive proof. I don't know if that's possible in Lean. The interpretation of proofs still assumes the consistency of their axioms.

There is no unconditional proof that CIC is sound. Thanks to Gödel, the best you can do is relative consistency proofs, something like "in ZFC with omega (i.e. infinitely) many inaccessible cardinals, you can prove that the theory of Lean is consistent". Such a relatively consistency proof can be fully formalized in Lean (and in fact, in much weaker systems than Lean).

I understand that, even taking Gödel's results into account, formalization helps us analyze mathematics and can lead to new (non-mechanical) ideas and results.

Do you honestly Jeremy Avigad (to pick one of the authors) isn't intimately familiar with the Incompleteness Theorems? For starters, Jeremy is chair in logic and philosophy of maths at CMU. https://www.andrew.cmu.edu/user/avigad/

Perhaps you'd like to explain how you think the Incompleteness theorems affect this project?

I think the comment was poking fun at the phrase, "to formalize all of mathematics".

That makes it sound like all possible mathematics past and future in all conceivable worlds. And we already know there are undecidable or unprovable statements, higher-order logics that cannot be fully formalized, concepts about axioms themselves that cannot be axiomatized, etc.

So it cannot mean "all of mathematics", strictly speaking. Just the areas in existing mathematics that have (or can have) formal proofs.

Well since one of the authors of TFA is literally the person who was asked by the association of symbolic logic to give the memorial lecture for Goedel’s centenary the comment could scarcely have been wider of the mark.

Feels like every time formalization is mentioned on hn somebody mentions incompleteness as though mathematicians in the field have never heard of it. It’s kind of annoying at this point. It’s like if every time we talked about a computer algorithm someone popped in to say “Have you heard of ‘On Computable Numbers’? Alan Turing would like a word.”

People in the field know about these things probably better than we do. They are aware of the consequences of completeness/incompleteness, decidability, computability etc. In fact Goedel’s completness and 2 incompleteness theorems have been formalized in lean as part of mathlib4 https://formalizedformallogic.org/Book/first_order/goedel1.h...

Great link, wonderful, Formalized Formal Logic. I'll enjoy reading through it. I see, a Japanese person worked on the formalization of Gödel's Incompleteness Theorems.

『Leanを用いたGödelの第一・第二不完全性定理の形式化』

..Oh I found a newer (more complete :) version of the proofs under the same domain.

https://formalizedformallogic.org/Catalogue/Arithmetic/G___d...

Looks like the /Book route is from an archived repo (https://github.com/FormalizedFormalLogic/book) and the content was moved to the Foundation's Catalogue. https://formalizedformallogic.org/Catalogue/

From the posted link, How to Formalize All of Mathematics, in the introduction:

> vision of how we can all work toward a world in which all, or almost all, mathematical definitions, theorems, and proofs are equipped with a formal representation

That "or almost all" feels like a wink to acknowledge the commonly misunderstood limitations of formal logic and systems. Your frustration is understandable, someone even wrote a whole book about it.

Franzén, Torkel. Gödel's Theorem: An Incomplete Guide to Its Use and Abuse

The incompleteness theorem doesn’t mean it’s impossible to formalize all of mathematics. It just means you’ll need to build out “various” mathematics from a landscape of axioms that are not necessarily all compatible with each other.

A bit like a multiverse of mathematics.

If we are going to formalize everything can we please do it in the style and spirit of the 1lab? https://1lab.dev

Oh how interesting, they're using a fork of Agda called Mikan, not Lean as I imagined before visiting the link. https://1lab.dev/Mikan.html

Yup, Mikan is a fork of Agda that focuses specifically on Cubical Type Theory. Lean's CIC is only one approach to dependent type based formal verification. Cubical gives you a computational approach to Homotopy Type Theory.

The biggest difference from Lean's CIC is how equality is handled. Lean's equality is Set like (allproofs of an equality are equal), whereas in cubical equality is higher dimensional. Equalities are paths and there can be multiple distinct paths between things. This means function extensionality and univalence are theorems that actually compute rather then be axioms or derived principles that get stuck. You also get higher inductive types "for free."

All that said I don't mention 1lab for the fact that it is Cubical. I think its a fantastic example of how to use dependent types to explore, teach, and formalize mathematics in a pro-human way.

I'd never heard of Cubical Type Theory, how interesting. Aside from that, and Mikan - why they forked, their development/contribution policy (which I happen to agree with more or less); and the notion of equality and equivalence (you didn't use this word but I read an article¹ with a glimpse into these concepts).. "Equalities are paths" - I'm going to be thinking about that for a while. Anyway the link to 1lab and the comments in this thread gave me various ideas to chew on, there's lot of substance there.

On the 1lab site, I started with simply-typed lambda calculus, an all-time classic that I've always wanted to understand more fully. How the site is designed, I love the syntax-highlighted math/code and the interface where every single concept can be clicked and hovered over to show additional information with usually a link to its own page. It led me to a kind of branching, graph-like manner of learning, where I open pages on categories, products, morphisms, uniqueness, equality - filling holes in my understanding as needed, then going back to more specific ideas built from those general foundational concepts.

An interactive textbook as a computational medium I feel has a lot more potential for usefulness and expression, to support an autodidactic and exploratory style of learning. It relates to topics raised elsewhere in this thread, like a "proper IDE for math" (integrated development environment for mathematics) and a language-agnostic "standard library" of data structures, algorithms, definitions, theorems, etc., where programming languages can import from a shared corpus of mathematically rigorous primitives.

> how to use dependent types to explore, teach, and formalize mathematics in a pro-human way

I find it meaningful how you phrased this - at this point in history with the state of technology that can overwhelm and devalue human intelligence, it's more important than ever to focus on how we teach, learn, communicate and cultivate understanding.

On a tangent, one of my interests is the book _Reflective Programs in Tree Calculus_² by Barry Jay, its proofs in Rocq, his more recent article "Typed Program Analysis without Encodings"³, and the work of his main collaborator⁴. I lack the relevant academic background to fully grasp it yet, so I've been chipping away at learning the necessary basics. So the link to 1lab is appreciated, it's a resource I'll be digging into over time.

---

¹ With Category Theory, Mathematics Escapes From Equality https://www.quantamagazine.org/with-category-theory-mathemat...

² https://github.com/barry-jay-personal/tree-calculus/blob/mas... (PDF)

³ https://github.com/barry-jay-personal/typed_tree_calculus/bl... (PDF)

⁴ https://github.com/lambada-llc/tree-calculus

What a wonderful response :)

> I'm going to be thinking about that for a while.

This is a deep and fascinating world to get into. Enjoy!

> It led me to a kind of branching, graph-like manner of learning...

Yes! I love this experience. It takes a little owrk but you can even import the 1lab as a library and re-implement whatever fragment of it you are trying to learn. Working through a proof using a proof checker is an amazing experience and is actually really fun.

The real learning (about the thing you are proving but also about type theory, programming language design, abstraction, etc) occurs while interactive with the proof checker. They all come with really sophisticated tools for interacting with the compiler and the code, interactions that are rather unlike any other ide experience.

If you wanted a place to get started I would highly recommend PLFA: https://plfa.github.io/

> An interactive textbook as a computational medium I feel has a lot more potential for usefulness and expression

I agree 100%. PLFA is a great example of something in that direction but I think we could go a lot further. I've fantasized forever about something like the illustrated primer from Neal Stephenson's The Diamond Age (https://en.wikipedia.org/wiki/The_Diamond_Age). I think that LLMs + dependently type languages could get you close to it.

Thanks for further recommendations. Programming Language Foundations in Agda. The Diamond Age by Neal Stephenson. I made a note to look into these.

Oh I see one of the authors of PLFA is Philip Wadler, whose name I recognize from Haskell and various papers on programming language theory. There's a Lean version of the book too. https://github.com/plfa/plfl

> Working through a proof using a proof checker .. They all come with really sophisticated tools for interacting with the compiler and the code

I have some prior experience developing a specialized code editor for a template language, and remember thinking at the time how much more potential there is for an advanced interface that supports the author, that deeply integrates with type information, documentation, examples, etc. Not just for writing programs and templates, but also for "rich text" and multimedia documents - for example, including music scores, diagrams, graphs.

Speaking of dependently typed languages (whose definition I admit I don't fully grasp yet), it reminds me of a paper I find fascinating and have read multiple times.

Physics, Topology, Logic and Computation: A Rosetta Stone - https://arxiv.org/abs/0903.0340

Again I lack the foundational concepts to really understand it to satisfaction. So I'm sure the resources you recommended will be useful on my learning journey.

If it really is formalized, it seems like the exact ideas would be able to be translated to and from any other sufficiently capable language without gaining or losing anything.

"sufficiently capable" is doing an insane amount of heavy lifting here. Like you can only interpret a theory into another one if the target is at least as strong as the source and even then "to and from" is a MUCH stronger condition that most pairs of theories do not satisfy.

Then when a translation exists the proofs can blow up in size to where you lose feasibility and understandability even tho they are technically still proofs.

Regardless of all that, I wasn't even bringing up 1lab because of the choice of language or type theory. I bring it up as an example of a pro-human way of presenting formalization.

You think a project that bans LLM contributions completely can be replicated in spirit by those who welcome it?

"How to rewrite all software in Rust"

As a kid I learned the basics of programming in primary school before learning any math notation beyond the absolute basics. Programming was:

- a strict, limited syntax to lego complex ideas together

- strictly one-dimensional (characters/words in lines)

- variables were written with the intention to speak their semantic role

Coming to math beyond primary school was hilariously emotionally challenging:

- A simple sum described with a sigma symbol: "What? why are you writing all over the place for a simple for-loop or reduce operation? why a specific symbol at all for a trivial +-aggregation?"

- having to help a first year math university student with finding an algorithm to a number packing/division problem: "nobody teaches data structures or dataflow despite the fact it would make things very much easier for everybody?"

- variable 'a', 'b' in complex formulas: "What happened to you? Does your parent not love you? why are you a faceless goon in a sea of other symbols? Stormtropper-ass naming attitude smh. Also making things harder on the reader to digest the algorithm you actually want to talk about so you can be lazy with your pen"

- "Is any old Tom, Dick or Harry just making up multi-dimensional symbols here for every micro algo they come up with?!"

My math skills are okay now, since university was littered with just verbal formal definitions, which made everything easier. From day one I was yearning for a more unified formalisation of everything that was shown to me (or even competing universal formalisations, like in programming languages!), especially since Mathematics seem equally defined by the found insights as it was by the idiosynchracies of the researcher and the math community as a whole. I dreamed of getting the culture out of math, to relieve it from that "impurity" and make it more like my experience in programming, where a basic algorithm could be understood in the abstract and ported to a variety of languages/abstractions/formalisations.

Anyway, that was a kid's dream. Am I better now, team lead at some software company and teaching yyounger people programming and math in my spare time? Nah, I still look at everything with eyes of "How can this be improved?", just the "looks like rubbish to me" attitude has marginally come down.

Reply on news.ycombinator.com