The Effort to Build the Mathematical Library of the Future

Every day, dozens of like-minded mathematicians gather on an online forum called Zulip to build what they believe is the future of their field.

They’re all devotees of a software program called Lean. It’s a “proof assistant” that, in principle, can help mathematicians write proofs. But before Lean can do that, mathematicians themselves have to manually input mathematics into the program, translating thousands of years of accumulated knowledge into a form Lean can understand.

more…

Tau.Neutrino said:

The Effort to Build the Mathematical Library of the Future

Every day, dozens of like-minded mathematicians gather on an online forum called Zulip to build what they believe is the future of their field.

They’re all devotees of a software program called Lean. It’s a “proof assistant” that, in principle, can help mathematicians write proofs. But before Lean can do that, mathematicians themselves have to manually input mathematics into the program, translating thousands of years of accumulated knowledge into a form Lean can understand.

more…

Oh, “pure” mathematics. LOL.

I have heard of software that can handle proofs in pure mathematics.

Here’s a ridiculous idea I had some five or so years back. All interesting proofs in mathematics involve infinity. Everything else is trivial. So just invent a consistent way of handling infinity (such as the Veronese continuum) and pop, all the proofs should fall out.

mollwollfumble said:

Tau.Neutrino said:

The Effort to Build the Mathematical Library of the Future

Every day, dozens of like-minded mathematicians gather on an online forum called Zulip to build what they believe is the future of their field.

They’re all devotees of a software program called Lean. It’s a “proof assistant” that, in principle, can help mathematicians write proofs. But before Lean can do that, mathematicians themselves have to manually input mathematics into the program, translating thousands of years of accumulated knowledge into a form Lean can understand.

more…

Oh, “pure” mathematics. LOL.

I have heard of software that can handle proofs in pure mathematics.

Here’s a ridiculous idea I had some five or so years back. All interesting proofs in mathematics involve infinity. Everything else is trivial. So just invent a consistent way of handling infinity (such as the Veronese continuum) and pop, all the proofs should fall out.

I should also add that there has been a major project in pure mathematics for decades to rewrite all the old proofs in modern language to both shorten the proofs, and check that they’re really correct.

mollwollfumble said:

mollwollfumble said:

Tau.Neutrino said:

The Effort to Build the Mathematical Library of the Future

Every day, dozens of like-minded mathematicians gather on an online forum called Zulip to build what they believe is the future of their field.

They’re all devotees of a software program called Lean. It’s a “proof assistant” that, in principle, can help mathematicians write proofs. But before Lean can do that, mathematicians themselves have to manually input mathematics into the program, translating thousands of years of accumulated knowledge into a form Lean can understand.

more…

Oh, “pure” mathematics. LOL.

I have heard of software that can handle proofs in pure mathematics.

Here’s a ridiculous idea I had some five or so years back. All interesting proofs in mathematics involve infinity. Everything else is trivial. So just invent a consistent way of handling infinity (such as the Veronese continuum) and pop, all the proofs should fall out.

I should also add that there has been a major project in pure mathematics for decades to rewrite all the old proofs in modern language to both shorten the proofs, and check that they’re really correct.

See also https://plus.maths.org/content/rewriting-enormous-theorem

> A group of mathematicians are part way through the Herculean task of rewriting the longest proof in mathematics – that of the classification of finite simple groups. When the proof was finally completed it was scattered over literally hundreds of journal articles and estimated at about 15,000 pages. So in the 1980s several mathematicians, initially Daniel Gorenstein and Richard Lyons, and then shortly afterwards Solomon, began to try to bring the proof together into one place.

And also https://www.sciencedirect.com/science/article/pii/0743106692900477

That paper is about using computers to prove theorems.

Remind me to read this in more detail later.