Hacker News Reader

Comment by drchewbacca | Hacker News Reader

I have done a little with http://us.metamath.org/ and I am sure within 10 years every professional mathematician will use formal proofs.

The two prerequisites are 1) making a fluid and intuitive interface for inputting proofs which can also display human readable proofs for any theorem known and 2) creating a database of all known mathematical proofs into which new results can be inserted.

Both tasks are ~50% complete. Metamath, for example, has all of mathematics formalised up to a basic undergraduate level. It has some reasonable editing software, but not close to good enough for mass adoption. There are also plenty of other systems being developed.

The time will come though relatively soon.

View on HN

> I am sure within 10 years every professional mathematician will use formal proofs.

I'll take that bet. 1:1 odds, up to $50? Shall we say, every mathematician employed at an ivy league university math department (postdoc level or above) has published at least one paper which employs proof checking for at least some claim? (provided that they have published at all.) So I win if I can find at least one professor or postdoc employed at an ivy league university math department on August 18, 2029, who has published at least one mathematics paper, and who has not published any mathematics paper which contains any formal proof.

That's a much weaker claim than yours, so it ought to be pretty generous to you.

I just wanted to note how precise of a bet this is. I will be stealing the exact definition of conditions and contexts to which the bet applies, to future bets of my own.

Yeah ok when you put it as a bet I think I'll back down ha ha :)

I imagine there will be hold outs who will never switch to formal proofs, though they may simply take on co-authors who are just "formalizers".

I also am probably being over confident with the time scales, I think a process with a tipping point, everyone will use it once everyone starts using it.

However when that tipping point will occur is probably hard to predict. I think it will be soon, but I'm broke and not that sure.

> I am sure within 10 years every professional mathematician will use formal proofs.

They said the exact same thing 10 years ago - see e.g. https://www.vdash.org and the AMS Notices special issue on formal proof from around the same timeframe. Formal proofs are hard, sometimes tedious and not always very intuitive. They're slowly spreading out from the most "synthetic" subfields of math (the ones where you're basically working with unfamiliar "rules", but not with a huge library of proven results), but progress is really slow - definitely slower than many people would expect!

Shouldn't it be written with Coq instead? Like UniMath[1] for example?

[1] https://github.com/UniMath

There are quite a few competing systems at the moment, as with all things software, each one wants to be the standard :)

https://jiggerwit.wordpress.com/2018/04/14/the-architecture-...

Reply on news.ycombinator.com