Rendered at 04:06:27 GMT+0000 (Coordinated Universal Time) with Cloudflare Workers.
ghm2180 12 hours ago [-]
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.
lifeisloving 11 hours ago [-]
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.
smashers1114 10 hours ago [-]
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.
lifeisloving 7 hours ago [-]
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".
sublinear 3 hours ago [-]
So... use a RAG trained on the books you care about?
11 hours ago [-]
ksd482 11 hours ago [-]
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.
pfdietz 9 hours ago [-]
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.
yunwal 9 hours ago [-]
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.
dataviz1000 10 hours ago [-]
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!
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.
fasterik 10 hours ago [-]
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.
nixon_why69 11 hours ago [-]
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?
jacobolus 10 hours ago [-]
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.
tzs 2 hours ago [-]
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.
"Reading" a textbook is very different from reading a novel, that should be noted. You gotta do the exercises.
NooneAtAll3 11 hours ago [-]
> - you can DM me -
...how?
ndriscoll 12 hours ago [-]
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.
jojomodding 5 hours ago [-]
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.
ndriscoll 3 hours ago [-]
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.
aeonik 5 hours ago [-]
Lemma, Theorem, Proof, Repeat.
lioeters 12 hours ago [-]
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.
joe_the_user 12 hours ago [-]
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.
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.
rramadass 12 hours ago [-]
Reminds me of the following papers (from 1979!) by Ernst Snapper;
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.
joe_the_user 11 hours ago [-]
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.
nyrikki 11 hours ago [-]
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.
osculum 13 hours ago [-]
Hasn’t this been tried already?
smitty1e 8 hours ago [-]
I thought Stephen Wolfram had already done some victory laps.
infamouscow 13 hours ago [-]
You might be thinking of the Langlands program
seanhunter 12 hours ago [-]
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.
You give me too much credit. I was just being tongue-in-cheek about Principia Mathematica.
transitorykris 13 hours ago [-]
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.
contubernio 12 hours ago [-]
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.
transitorykris 11 hours ago [-]
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.
shiandow 12 hours ago [-]
> 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.
N_Lens 13 hours ago [-]
Godel would like to talk to you about his “Incompleteness Theorem”
dwohnitmok 13 hours ago [-]
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.
Maxatar 12 hours ago [-]
>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.
dwohnitmok 8 hours ago [-]
> 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.
netdevphoenix 12 hours ago [-]
Then, "All of Mathematics" is being used as clickbait.
dwohnitmok 8 hours ago [-]
I pretty strongly disagree. The body of the text was what I expected based off the title.
epgui 11 hours ago [-]
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.
LPisGood 12 hours ago [-]
If a theorem has a published proof, it is either formalizable or incorrect.
fdupress 12 hours ago [-]
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.
LPisGood 12 hours ago [-]
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.
fpvandoorn 11 hours ago [-]
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).
whatshisface 12 hours ago [-]
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.
Maxatar 12 hours ago [-]
[dead]
seanhunter 12 hours ago [-]
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?
lioeters 11 hours ago [-]
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.
seanhunter 11 hours ago [-]
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...
lioeters 9 hours ago [-]
Great link, wonderful, Formalized Formal Logic. I'll enjoy reading through it. I see, a Japanese person worked on the formalization of Gödel's Incompleteness Theorems.
『Leanを用いたGödelの第一・第二不完全性定理の形式化』
..Oh I found a newer (more complete :) version of the proofs under the same domain.
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
wslh 12 hours ago [-]
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.
fedeb95 13 hours ago [-]
Also Chaitin would like a few words.
lioeters 13 hours ago [-]
The Limits of Mathematics: A Course on Information Theory and Limits of Formal Reasoning - Chaitin, Gregory
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."
vngzs 12 hours ago [-]
[dead]
NooneAtAll3 11 hours ago [-]
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
solomonb 12 hours ago [-]
If we are going to formalize everything can we please do it in the style and spirit of the 1lab? https://1lab.dev
hyperhello 11 hours ago [-]
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.
solomonb 10 hours ago [-]
"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.
lioeters 12 hours ago [-]
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
solomonb 11 hours ago [-]
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.
voxl 7 hours ago [-]
You think a project that bans LLM contributions completely can be replicated in spirit by those who welcome it?
solomonb 6 hours ago [-]
[dead]
UltraSane 12 hours ago [-]
Formally verifying all of math would be an amazing achievement by humanity.
whywouldyoucare 11 hours ago [-]
V.I. Arnol'd: "Only fools prove theorems."
(The wording may not be exact, though the sense should be.)
UltraSane 11 hours ago [-]
Do you think this silly comment is somehow profound? Math is mainly about proving theorems true or false or finding counterexamples.
whywouldyoucare 10 hours ago [-]
And nevertheless this is what Arnol'd said. Do you also think he was silly?
UltraSane 8 hours ago [-]
Yes that is an extremely stupid thing for a mathematican to say and pointless to quote.
bossyTeacher 10 hours ago [-]
Title isn't true. It is a subset but clickbait gotta clickbait.
Silamoth 9 hours ago [-]
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.
bossyTeacher 8 hours ago [-]
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.
Silamoth 6 hours ago [-]
At best that seems like a nitpick based on a specific notion of “all of mathematics”. Care to explain what you mean?
lioeters 2 hours ago [-]
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.
fithisux 11 hours ago [-]
$ChatGPT> "How to Formalize All of Mathematics?"
AI has all the answers. Why read the article?
stabbles 13 hours ago [-]
"How to rewrite all software in Rust"
nyrikki 11 hours ago [-]
[dead]
noah_reads 11 hours ago [-]
[flagged]
ozereray1 13 hours ago [-]
[flagged]
rf15 54 minutes ago [-]
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.
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.
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.
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".
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.
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
AI labs definitely should work on it.
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?
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/
...how?
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.
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.
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.
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.
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, 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.
> “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.
Here's a really good and accessible intro to Langlands https://www.youtube.com/watch?v=4dyytPboqvE
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.
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.
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.
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.
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.
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.
A bit like a multiverse of mathematics.
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.
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.
Perhaps you'd like to explain how you think the Incompleteness theorems affect this project?
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.
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...
『Leanを用いたGö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
https://ia801804.us.archive.org/35/items/A-Z_Library_G-K_Jos... (PDF)
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."
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
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.
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.
(The wording may not be exact, though the sense should be.)
You cannot formalize ALL of mathematics. We have known that for a while. Hence my point about the title being clickbait.
AI has all the answers. Why read the article?
- 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.