13
$\begingroup$

The choice of the proof assistant to use for formalisation depends on the area quite a bit; e.g. they say that algebraic topology comes easy in HoTT assistants.

What would be the most natural choices for combinatorial constructions in the spirit of, say, block designs/Steiner systems. That is, where one explicitly manipulates subsets of a fixed finite set to establish basis for induction, or, say, proves that the 1 and 2-dimensional subspaces of a 3-dimensional vectorspace over a finite field $\mathbb{F}_{q}$ satisfy axioms of a projective plane.

These constructions might also involve manipulating, say, identities among certain polynomials modulo ideals, e.g. elements of finite group rings.

EDIT: It would also be beneficial to be able to extract implementations and actually generate examples of these objects.

Improve this question
$\endgroup$
2
  • 6
    $\begingroup$ synthetic algebraic topology comes easy in HoTT assistants! The algebraic topology I learnt as an undergraduate had the real numbers playing a central role. $\endgroup$
    – Kevin Buzzard
    Commented Feb 14, 2022 at 19:23
  • 6
    $\begingroup$ Agreed. Actually, I prefer to say "synthetic homotopy theory" -- once you make it synthetic, there's arguably not much "topology" left in it except for some vestigial words like "path". And "comes easy" is a bit of an understatement -- synthetic homotopy theory can only be done in HoTT, almost by definition. $\endgroup$
    – Mike Shulman
    Commented Feb 14, 2022 at 22:31

2 Answers 2

Reset to default
7
$\begingroup$

If I understand you correctly, you will be working with finite discrete objects, such as finite fields, finite groups, finite combinatorial objects, etc. I would recommend using a proof assistant based on classical logic. There is little to be gained by studying finite discrete structures in a constructive setting.

Two proof assistants that would fit the bill are Isabelle/HOL and Lean.

Improve this answer
$\endgroup$
3
  • 2
    $\begingroup$ proofs there are mostly constructive, though. And it would be fun to extract these constructions and actually generate objects... $\endgroup$
    – Dima Pasechnik
    Commented Feb 14, 2022 at 20:58
  • 3
    $\begingroup$ Should it not be possible to use $\Pi^0_2$-conservativity of classical arithmetic over intuitionistic arithmetic to extract algorithms from classical proofs? Or to put it in less fancy terms, won't all (most?) uses of excluded middle be harmless and algorithmically justified? $\endgroup$
    – Andrej Bauer
    Commented Feb 14, 2022 at 21:01
  • $\begingroup$ in more practical terms, it seems that Lean's proof extraction facilities are not really available. Not sure about Isabelle/HOL. $\endgroup$
    – Dima Pasechnik
    Commented Feb 14, 2022 at 21:16
4
$\begingroup$

I moved this answer to Proof assistants for beginners - a comparison, since it is general advice. However, I still do think it applies to your circumstance. In particular, it is not clear in your question what your end goal is and this probably effects your choice of proof assistant more than the particular mathematical topic you wish to formalize.

Improve this answer
$\endgroup$
4
  • $\begingroup$ I think this piece of advice is excellent. OTOH, it does not really answer the question. It could serve as an answer to this other question (or this one, for that matter), and I'd be willing to upvote it there. But it seems misplaced here, and hence I'd consider to downvote. $\endgroup$
    – Pedro Sánchez Terraf
    Commented Feb 15, 2022 at 1:48
  • 1
    $\begingroup$ @PedroSánchezTerraf I moved the answer as you suggested and left a short explanation of why I think my general advice applies in this case. $\endgroup$
    – Jason Rute
    Commented Feb 15, 2022 at 3:09
  • $\begingroup$ Oops, now you have 2 upvotes :-) $\endgroup$
    – Pedro Sánchez Terraf
    Commented Feb 15, 2022 at 3:12
  • 2
    $\begingroup$ As normal in academia, one does not know the end goal. :-) I did some work on verifying combinatorial constructions "by hand", arxiv.org/abs/1601.00181 - but there should be a better way, so I'm experimenting with students... $\endgroup$
    – Dima Pasechnik
    Commented Feb 15, 2022 at 6:24

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.