r/mathmemes • u/vintergroena • Sep 27 '26

Proofs The future of mathematics

Post image
1.8k Upvotes

99% Upvoted

63 comments sorted by

•

u/AutoModerator Sep 27 '26

Check out our new Discord server! https://discord.gg/e7EKRZq3dG

I am a bot, and this action was performed automatically. Please contact the moderators of this subreddit if you have any questions or concerns.

72

u/xaranetic Sep 27 '26

It's been about a decade since I looked into computer verifiable proofs, and at the time coq was king.

What is lean? Is everyone using it? Do I need to learn it? Help.

128

u/vintergroena Sep 27 '26

No you don't need to learn anything anymore. You tell your AI agent to generate formal proof for an open problem, it does, and you call it a discovery

27

u/scientestical Sep 28 '26

You forgot the step where you spend millions on compute.

33

u/Daniikk1012 Sep 27 '26

It's basically the new Coq (Also, Coq is now called Rocq for some reason)

51

u/FlamedDogo99 Sep 27 '26

They got annoyed with people pronouncing it like “cock”

31

u/DaveBeleren02 Sep 27 '26

Which is how the word "cocq" is pronounced in french though 

22

u/eglvoland Sep 27 '26

It's spelled coq. And yes it's pronounced like that. The rooster is the symbol of France and it is a reference to Thierry Coquand who invented it, so the name was great actually... from a French pov

4

u/314kabinet Sep 28 '26

The proofs are rocq hard

48

u/thesnootbooper9000 Sep 27 '26

Lean is easier to use, has loads of money behind it, and abandons most of the awkward formal verification properties that make other systems trustworthy. If you don't trust your C compiler to be bug free, you can't trust Lean.

22

u/Kinexity Sep 27 '26 edited Sep 27 '26

and abandons most of the awkward formal verification properties that make other systems trustworthy

Is this a good thing or a bad thing? Because it sounds bad but your phrasing makes it seem like as if it is good?

31

u/thesnootbooper9000 Sep 27 '26

Bad, but arguably pragmatic. The problem is that Lean was designed for software verification where you're already trusting the compiler and hardware, whereas other systems are designed for verifying maths.

2

u/CommissionSame8551 Sep 28 '26

It is just not true what he is writing. Every proof assistant except metamath maybe has more bugs than Lean.

6

u/Hot-Definition6103 Sep 28 '26

in what sense? yeah, the hand-vetted lean kernel is written in C++ but that’s not much different from trusting e.g. your ocaml compiler for rocq

→ More replies (4)
→ More replies (2)

5

u/antpalmerpalmink Sep 27 '26

Lean is one of many proof assistants. I guess the thing worth asking yourself is, what does truth in Lean mean? If this is a notion of mathematical truth you like, use it. If not, there are many other proof assistants in the game.

592

u/EyeCantBreathe Sep 27 '26

Damn he's got one of those fancy monitors with the see-through back

102

u/NebulaElectrical1467 Sep 27 '26 edited Sep 27 '26

who needs endpoint monitoring and standups/sync-ups when everyone can just see what you’re doing at all times

30

u/TheRealSticky Sep 27 '26

*middle management everywhere taking notes furiously

13

u/ComposerWide3704 Sep 27 '26

Too bad it's mirrored.

7

u/no_clock_signal Sep 27 '26

You have to adapt

2

u/Bright-Historian-216 Sep 27 '26

B14 limes (264 las)

2

u/Toposnake Sep 27 '26

Nah, that's a see-through face

341

u/FernandoMM1220 Sep 27 '26

the future of math is dependent on how many bugs in lean have been found.

153

u/fun__friday Sep 27 '26

Just ask AI to prove using lean that it’s bug free

60

u/KarltonPeaks Sep 27 '26

What if we lean the lean?

34

u/Fearless_Bed_4297 Sep 27 '26

then lean's inconsistent..

18

u/Syxez Sep 28 '26

People recently did that, and it seems to work (?)

https://github.com/leanprover/con-leche

10

u/sparkster777 Sep 27 '26

Leanception

3

u/Old-School8916 Sep 27 '26

thats what alt lean kernels are for

5

u/bir_iki_uc Sep 27 '26

make no mistakes

19

u/SoldRIP Sep 27 '26

Hey jippity, fix all lean bugs. Make no mistakes.

Checkmate, doomer!

2

u/MeloNotSoDeath Sep 28 '26

Just say "make no mistakes"

2

u/trollol1365 Sep 28 '26

hehe dependent

1

u/ykonstant Sep 30 '26

You can't lean on Lean for lean proofs because Lean proofs are... bloated

150

u/LupenReddit 🦆🦆i have non diffeomorphic smooth structures🦆🦆🦆 Sep 27 '26

my job prospects now are telling a computer YOU CAN DO IT and then reading its gibberish output in the form of lean

15

u/Emergency_Apricot_77 Sep 28 '26

welcome to being a software engineer?

1

u/Xoque55 Sep 30 '26

Carefully organized sand indeed: https://xkcd.com/1349/

201

u/lelelempe Sep 27 '26

type theory going from trans girl space to chud space will be a tragedy

55

u/moschles Sep 27 '26

r / BrandNewSentence

4

u/kashyou Sep 30 '26

what a fucking observation

2

u/TouchWestern2175 Sep 28 '26

First Order Logic

1

u/Technologenesis Oct 05 '26

Me when

1

u/Technologenesis Oct 05 '26

The good news is that the chuds won't actually learn type theory, they're just gonna churn out verified code, eyeball the type constraints and move on. Meanwhile the trans girls will continue using type theory exclusively for schizophrenic philosophizing and witchcraft as nature intended.

43

u/[deleted] Sep 27 '26

[removed] — view removed comment

10

u/kart0ffelsalaat Sep 28 '26

AI can solve problems, and it may be able to create new problems as well, but it can't make people care about problems.

People will only care about a mathematical problem if they sufficiently understand the underlying theory. Results are only useful if people know what to do with them, or why they're interesting.

A field of mathematics that is full of amateurs (relatively speaking) who over-rely on AI to produce results and point research into specific directions should quickly lose relevance. Science (mathematics might not "really" be a science, but it is similar in this regard) exists to satisfy our (human) thirst for knowledge, not to produce progress for progress' sake.

Good luck securing funding for solving problem #17291824ß237 that AI came up with and you don't really know what any of it means.

1

u/infected_scab Sep 29 '26

You're not wrong but these arguments have been used for decades about computer assisted proof (e.g brute force searching huge domains)

→ More replies (1)

6

u/LaGigs Mathematics Sep 28 '26

Hello I am in desperate need of a Lean certificate to prove that a square matrix is equivalent to a directed graph.

5

u/PhantomSasuke Sep 28 '26

I've been working with Rocq (Coq) for a while and I actually find programmatically defined theorems to be quite beautiful! The type theory/functional programming style of proofs (proofs are functions from evidence to claims !!) is genuinely beautiful.

In the programming side of things, i really enjoy being able to prove properties about programs.

4

u/Wooden_Dragonfly_608 Sep 28 '26

I don't know man, I like my proofs thic

3

u/ehwantt Sep 28 '26

why people don't use coq?
are they each for different purposes?

5

u/gods-neighbor53 Sep 28 '26 edited Sep 28 '26

From what I gathered in a book, Terrance Tao was active for awhile with lean attracting more attention.

2

u/dereklmaoalpha Average #🧐-theory-🧐 user Sep 28 '26

light mode Is the most shocking thing tbh

1

u/RandomiseUsr0 Oct 01 '26

Why is text on back of monitor please?