How to Formalize All of Mathematics

N_Lens

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

osculum

Hasn’t this been tried already?

transitorykris

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.

stabbles

"How to rewrite all software in Rust"

solomonb

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

rramadass

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.

ndriscoll

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.

ghm2180

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.

UltraSane

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

fithisux

$ChatGPT> "How to Formalize All of Mathematics?" AI has all the answers. Why read the article?

NooneAtAll3

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

bossyTeacher

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

rf15

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.