Home | Notifications | New Note | Local | Federated | Search | Logout

Note Detail

Lynne@lynne@mk.pars.ee (2026-10-07 19:54:17)
I think that this is the starting point where mathematics becomes an API, with Lean formalization coming first, which then gets distilled by agents (guided by humans, currently), fit inside giant Lean libraries, with the points that made the proof work extracted and taken as proven by other agents to prove more problems, 20 goto 10.
Agents will keep extending proofs further, like Turing-complete Navier-Stokes was, on their own (with human guiding for now).
It takes a fraction of the mathematics community to learn how to prompt and treat mathematics like a startup to completely disrupt everyone else. I keep seeing mathematicians in their "bargaining" stages of grief, so I feel like its happening.
---Reply---
Lynne@lynne@mk.pars.ee (2026-10-07 19:58:04)
Programmers went through this exact same process mere months ago. I don't feel bad for them. I don't feel bad for mathematicians either. I don't feel bad for biologists, who I think may be next, with lights-out wet labs coming online.

---Replies---

Sun Microdevil Pte Ltd@koakuma@uwu.social (2026-10-07 20:04:34)
@lynne Where do we get AI that generates so much food and optimally distributes them that we as a society don't have to work anymore just to survive

Personally that would be the really interesting part to witness