Script to generate a list of Most Wanted Implications

[mrinesi]

Based on the comment at https://terrytao.wordpress.com/2024/09/25/a-pilot-project-in-universal-algebra-to-explore-new-ways-to-collaborate-and-use-machine-assistance/#comment-685879

[Caveat: quick-and-dirty proof of concept, not production-ready code]

Takes as input a .lean file parseable in the project's format, and generates a Markdown file with a list of potential implications a ->b of currently known value sorted by "interestingness" (|ancestors of a| + |descendants of b|).

This is straightforward, but there are alternative metrics that might be more interesting (e.g. this only considers "what if the implication is true," not "what if it's not"). From first principles one might want to give priority to edges that maximize information gain in the sense of leading to closures with fewer unknown edges once we know their true value, non-greedy heuristics like trying to build bridges between non-adjacent graph components, etc.

[teorth]

Some weird problem with getting the blueprint to compile with your PR... possibly updating to the latest blueprint will help?

[pitmonticone]

Yes, exactly. @mrinesi you just need to push another commit and the checks will pass.

[mrinesi]

@pitmonticone Fantastic, it does pass now.