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.
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.