Hi all, I'd like to introduce a new tool which might help communicate and coordinate efforts around Metamath: *Blueprints*
https://tirix.github.io/metamath-blueprints/ The set.mm database only includes fully validated and verified theorems. However, in many cases, it is interesting to discuss the path forward, and e.g. definition choices. This has been done using commented out theorems in the database, but blueprints might be an alternative. In the Metamath community, there are both: * people who are used to formalize proofs in set.mm or iset.mm, know the tools, * people who are used to mathematics, have access to math litterature, and know the fundamentals. In some cases people fall in both categories, but not always. Blueprints is a way to help communication: * explaining the path to complex theorems, and showing what's left to formalize, even for one single contributor, for the rest of the community, * organizing, coordinating and e.g. splitting larger tasks between several contributors, * communicating larger proofs and concepts between mathematicians and formalizers, * viewing and tracking the progress made in a project Blueprints are used extensively in Lean (see for example https://terrytao.wordpress.com/2023/11/18/formalizing-the-proof-of-pfr-in-lean4-using-blueprint-a-short-tour/), and I believe that Metamath can benefit from a similar tool. In order to create new blueprints edit existing ones, all you need is to edit the files in https://github.com/tirix/metamath-blueprints. That can be done comfortably directly in GitHub. I'll use it in the future to present and communicate the way I want to go forward: feel free to try it too! _ Thierry -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/2fd9160a-d7a7-4f4a-92d5-94577d3940ee%40gmx.net.
