Hacker News new | past | comments | ask | show | jobs | submit login

It seems like encoding ‘all of math so far’ in some theorem prover seems like an ideal open source project where lots of people can make small contributions which don’t require a vast amount of mathematical knowledge — you’d mostly be simply encoding other people’s results. Is there such an effort now?





I tried to do something like that (http://proofpeer.net), but got lost in the details. Learnt a lot from it, but implementing your own cloud versioning system is probably more appropriate for a project with 100 million dollars funding, not 600000 pounds, half of which goes to university bureaucracy ;-)

I think formal abstracts (https://formalabstracts.github.io) is promising in principle (it doesn't focus on proofs though).

The Archive of formal proofs (https://www.isa-afp.org) is the biggest effort I know, but the logic (Isabelle/HOL) is not powerful enough for doing advanced mathematics comfortably, and the process of contributing is quite arcane.


> It seems like encoding ‘all of math so far’ in some theorem prover seems like an ideal open source project... Is there such an effort now?

Yes. Metamath's set.mm is expressly such a project, and I recently created a Gource visualization of set.mm's progress over time. For the first few years it was basically one person, but that increased over time and there have now been 48 different contributors.

See:

https://www.youtube.com/watch?v=XC1g8FmFcUU


https://formalabstracts.github.io/

Tom Hales' formal abstracts project may be to your liking.




Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact

Search: