Blueprints for Metamath
Thierry Arnoux
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
savask
Thierry Arnoux
Great!
I will try to add more Geometry blueprints, I think the next one
could be Pythagoras.
I would also love you see you help in Algebra, and maybe even in
Geometric Algebra.
One question - will the metamath statement be pretty-printed if it's in the "statement" field of the blueprint?
It's not the case currently but it can be added. I would then link the blueprint with a database, so that some information can be retrieved from the database.
_
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/223c5216-d370-422a-8ae9-0600ba2c1875n%40googlegroups.com.