On Math Platform
I was thinking a combination of mathematics as a collaborative game (simulations) and engineering mathematics. A platform with the map of mathematics as well as the pull request capability — that could take an idea (or a group of ideas and insights), that kind of seed, modeled as an e-graph (or something similar), given the mathlib-like math knowledge base context, to something that gets formalized, and is fully reusable. With enough compute, one could get agents to work on that thing in the background — it’d become a small island (rather than only a point) in that special embedding space.
One could feel a bit more like an artist (again), and not fully know how far the AI could them help take a combination of insights, and some meta-code. Or how much their tool (in somewhat unexpected ways) could help or helped autoformalize something on the other side of the globe. Let’s say someone wrote a new way to assign colors to numbers. That’s not immediately usable for human mathematicians, but could be used as a feature by the AI (that does not sleep and likes to read at a tough-to-imagine scale).
That kind of new way of doing math that involves:
Code with AI — global math programming language, the ecosystem, use cases, connectors / drivers, help from the agents, chat with the codebase and so on, more robust plugins and code completion, meta math API for other APIs,
Git — math structures could be represented like chemical compounds, or like in Lean, and made concise and readable in text form ; what matters is that the software side of math engineering works at scale,
Collaboration — collaboration will be a major difference, it should work like it works with software; it could even get better through next-gen recommender systems, highly distributed, communication and transparency is key here,
Seeding — the first insight can be generated, or come from a human, the UX will matter a lot, i.e. how people sketch ideas, discover facts, create conjectures; seeding reminds me of prompting in some ways, but it requires deeper thought and more energy from the user,
Flexibility — connecting code and data, with language models, connecting people, bootstrap-like code to start with, simple UX around idea co-creation (with AI) and sharing / getting feedback,
Agents — doing the translation and the basic work, providing conjectures, updating the next-gen blueprint, working in the background, creating new knowledge base + getting feedback from advanced users (so that it’s clear what’s worth looking into),
Personalization — you can provide value at any point of your life, you get can feedback on your ideas, your ideas would be a chain of ideas in some larger context, with the audit log (checkers, formalization tools, autoformalization tools, and so on),
Verification — making things reusable, a bit like TDD + CI/CD for math programs, every step should be verified, cron jobs, checker tools, AI-based notes and notifications,
Applications — connecting use cases, tools, other branches of science, simulators, it should perhaps just run on a desktop (still, it should probably start as a website); I’ve built a small desktop tool for own notes as well as a Lean assistant for myself back in the day, but I guess having one app for everyone would matter,
Attribution — the chain of authors, currently Hamilton is not included in the name Ricci flow, and there must be thousands of examples like this; the idea chain can be documented (in many ways) at scale; there could exist labels, but there also must exist idea chains,
Projects — I would, for instance, create a project related to electromagnetic waves, and try to build tools around that; it’d feel a little bit like Minecraft or Roblox when it comes to simulations, and — of course — only few nodes would run such heavy simulations,
Hardware — math insight pills of some sort; I wrote an article about that kind of digital net-based hardware; that will probably take some time, but it could essentially be an efficient way of capturing context-aware compute (think a reasoning chip that could be inserted into other devices)
At scale.
That kind of thing could be launched as a project where:
People share their ideas — that’d work like an editor and github, with some Lean, some natural language, some help from the agents,
AIs do the initial quality checks and then forward the insight pills (ideas and artifacts) to other mathematicians (the AI will estimate the depth of the insight, and forward the insights to the mathematicians who might be interested in reviewing it, the pull request way),
All people who “join” a specific project can work on it, and there’s some ranking system in place, and some roles.
Now, all this feels like a collaborative game. You can get a bunch of points for cracking the RH.
For every game (of a certain size, in terms of the speed of winning strategy generation given a certain context manifold), the interface between the AI and humans should, in principle, allow:
AIs to be able to judge human moves,
AIs to play against other AIs and humans, and learn in order to develop significantly better strategies (AIs will need to get better at learning (and thus recovering) quickly after failing),
Humans to learn by comparing their moves with better options.
It’d feel not only like a personalized teacher that could elevate everyone, but also a source of energy that could saturate millions of games. It’d be like watering the seeds (or later, the flowers). You water the seed and then take care of it, but can never fully understand it when it becomes a flower (its context is different — even if you both learn the whole time).
When it comes to math, the goal of the game would be to find the fastest possible way to turn insights and context into a more formal argument, and then merge that new knowledge into the global mathematical repository that can be used by the humans and the AIs using the plaform.
A game with such dynamics will lead to:
The average players getting better,
The best players getting (even way more) better,
The best players (and learners) becoming close to unbeatable,
The development of new strategies (and new games),
More on-demand problem and learning path creation,
Autonomous self-learning AI mathematicians,
Insight estimation algorithms and modern recommendation-driven collaboration,
Unification of theories and making them accessible through code,
Hopefully, cracking some big conjectures and creating new amazing theorems.
But the key here is autonomous software, collaboration, automation, a global network of mathematicians (the project would democratize math a bit as well as add structure and AI peer review into the pipelines), and a global knowledge base full of reusable pills. When I first learnt about Lean and Mathlib, I felt so inspired!
Dealing with deeper concepts high in the cosmic ladder (I guess prof. Terence Tao coined this term many years ago?) will require the next-level compute and collaboration. Math is about creation and building bridges, but in a very rigorous environment. Given the thing that can be explored is vast and counterintuitive, it feels like certain bridges between 10^1 an 10^10 will be different than those that apply to 10^1000000 - 10^10000000.
Scale of compute, to a certain extent, defines civilizations. Lifespan and human body are two such features of scale. Coming up with new high-coverage, high-leverage, deep-truth, highly-reusable math is so hard that we should use just any tool that could help. One could even think of i, or negative probabilities, or things like the Bunkbed conjecture that seem “obvious” only to be later disproved (or things like the Monty Hall problem that are so counterintuitive that few believe in them until they essentially hold their own universe in their hands) — deep truths at scale, even our scale, are hard to capture.
I recently learnt about the Equational Theories project (led by Tao, Monticone, Srinivas), and tried to do a couple of small coding experiments. When one looks at the expected types of compactness in the ET project, i.e. ⊢ ∀ {α : Type} [inst : DecidableEq α] {Γ : Ctx α} {E : MagmaLaw α}, models Γ E → ∃ Δ, Nonempty (models (ToCtx ↑Δ) E), completeness, i.e. ⊢ ∀ {α : Type} (Γ : Ctx α) (E : MagmaLaw α), models Γ E → Nonempty (derive Γ E), or models in MagmaLaw, i.e. ⊢ {α : Type} → Ctx α → MagmaLaw α → Prop, one gets to really appreciate:
1. The idea of how any data, esp. with some deeper truth in it, could potentially be turned into a program,
2. How a deep thought could now be encoded, and made ready for the machines to use.
The platform I am talking about would essentially be a math-producing machine oiled and co-created by humans. It would develop its own language, but the translator pipelines would be good.
Something like that could potentially feel like a digital version of time. Well, it’d still be a layer on top of time at first, but could eventually evolve into something more fundamental.
While experimenting, I had a look at Equation 14 and its dual (Equation 29), i.e. abbrev Equation14 (G: Type _) [Magma G] := ∀ x y : G, x = y ◇ (x ◇ y) and abbrev Equation29 (G: Type _) [Magma G] := ∀ x y : G, x = (y ◇ x) ◇ y. The original solution of 14 included that one special sentence, “The proof resembles the pattern-matching performed by Macro Preprocessors in Compilers for Computer Programming Languages like C”.
That reminded me of two things:
Scale (especially after reading the discussion around (from my perspective the “macro preprocessor”) way of capturing finite magmas’ and laws’ patterns through the concept of adjusted degrees of freedom),
My recent take on digital nets and presenting them as processors the computer architecture way.
That kind of machine could be built now.