3 ms·
Check out Metamath; we can do this for any serious foundations: http://us.metamath.org/downloads/metamath.pdf http://us.metamath.org/downloads/metamath.pdf
by EtDybNuvCu 9y ago
Check out Metamath; we can do this for any serious foundations: http://us.metamath.org/downloads/metamath.pdf http://us.metamath.org/downloads/metamath.pdf
- pacala 9y agoHave somebody done it for the more general foundations based on category theory? If I understand correctly, Metamath is a set of tools enabling such a formulation, but not the formulation itself. See ML vs. theorem prover implemented in ML.
- mbid 9y agoThere are some developments, for example "Globular": https://arxiv.org/abs/1612.01093 https://arxiv.org/abs/1612.01093 I don't think there is a proof assistant that's really based on categorical foundations. I'd love to see something like that though.