Hacker News Reader

Comment by marwahaha | Hacker News Reader

[dead]

why does the website force people to log in to see the proofs? also, why does it not have something like a "export all lean" button to download all of the lean code that proves a theorem (dependencies included) so it can be easily checked offline? finally, the campaign you gave has a mission "Integer Multiplication in O(n (log n)^(1-κ)) Time" and it's listed as completed, but i checked the graph and it directly depends on something that's listed as "Open" ("Full multiplication bound at κ = 0.000051016920170078"). is it fair to call it completed then?

Thanks for checking out the site. All of the Lean that is generated with an open-source license is exported daily here: https://github.com/prove2me/formalpedia

The graph has an AND-OR structure. Each node (circle) is a theorem statement, and each directed hyperedge (square) is an implication. To prove a theorem statement, all of the children of one implication must be proved.

It's missing a privacy policy, so not sure why you require login for users

I wasn't sure if this was necessary. What do you think would be useful to include in a privacy policy?

- What personal data you process and retain (login details, access logs, statistics, etc.)

- How long you retain it

- Who (which human, name and email) to contact when you have questions

- Which third parties get the data (if you use Google fonts, Google would be one of those, since it gets the users IP), etc.

That's the sort of default stuff that must be in a privacy policy, there are a few more things that you'd need to comply with GDPR and the UK's equivalent, but that's the kind of thing you need. :)

Reply on news.ycombinator.com