Comment by mariofdistrust

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?