Skip to main content
13 votes

Tutorial implementations of NbE

Daniel Gratzer has written two tutorial implementations of normalization by evaluation in OCaml: https://github.com/jozefg/nbe-for-mltt: plain MLTT with universes https://github.com/jozefg/blott: a ...
Jonathan Sterling's user avatar
10 votes

Formalizations of unsolved problems

The closest to what you are asking for might be the Formal abstracts project whose aim is to formalize the statements (but no proofs) of results from papers. Formalizing statements without proofs is ...
Andrej Bauer's user avatar
  • 9,593
9 votes
Accepted

Is there an official recommendation for editors to input Lean unicode characters?

Because maintaining such a big list of Unicode abbreviations is annoying and none of the editor mode maintainers are interested in encouraging untransferrable abbreviations, as far as I know, all of ...
Mario Carneiro's user avatar
7 votes
Accepted

verifying combinatorial constructions - choice of a proof assistant

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 ...
Andrej Bauer's user avatar
  • 9,593
7 votes
Accepted

What mathematical topics should I learn first before I start using proof assistants?

I came to proof assistants from TCS about a year ago, so perhaps I am well placed to answer your question. This may be somewhat opinion-based, but I don't feel it is necessary to learn category theory ...
Bolton Bailey's user avatar
7 votes
Accepted

How to deal with Binders?

There are already a lot of choices pointed out on Jesper Cockx's blog. Usually, the properties you would like to establish includes Equations of compositions of substitutions. For example, $E[x/A][y/...
Trebor's user avatar
  • 4,015
6 votes
Accepted

How could I make a Proof Assistant?

There are many good resources, such as the little prover book, "A tutorial implementation of a dependently typed lambda calculus" tutorial, "A simple type-theoretic language: Mini-TT&...
ice1000's user avatar
  • 6,276
6 votes

What mathematical topics should I learn first before I start using proof assistants?

I would say the most confusing (and often frustrating) notion for many first users is that types are not sets, so unless you plan on using a proof assistant specifically based on set theory (almost ...
Couchy's user avatar
  • 2,271
6 votes
Accepted

How to deal with the proliferation of encodings of ASTs?

As various commenters have said, you sometimes just need to bite the bullet. Good modularity, good naming conventions and other standard good software practices will help. If you need inspiration, I'...
Michael Norrish's user avatar
4 votes

Type Theory research groups

External links The following pages mention researchers interested in the foundations or applications of proof assistants: Authors participating in the TYPES international conference on Types for ...
4 votes

verifying combinatorial constructions - choice of a proof assistant

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 ...
Jason Rute's user avatar
  • 8,960
4 votes

What mathematical topics should I learn first before I start using proof assistants?

Here are some topics I would recommend learning: Some Functional Programming. I think it is good to learn some functional programming language. Preferably some language which takes immutability ...
Agnishom Chattopadhyay's user avatar
3 votes

Why use records for non-empty lists rather than inductively defined non-empty lists?

Since nelist_b is based on pre-existing lists, you can presumably reuse a lot of results on lists when proving facts about ...
Ana Borges's user avatar
3 votes

General Guidelines and Tips for using Induction

The best guideline is: If you don't know how to do the proof on pen-and-paper, you probably will get lost doing it in a proof assistant. If you don't know what your induction hypothesis is supposed ...
Jason Gross's user avatar
  • 1,537
3 votes

What mathematical topics should I learn first before I start using proof assistants?

Unlike the other answers, I'm fairly convinced you do not need to learn anything (category theory, type theory, functional programming, or even logic) before hand. I have two basic reasons for this. ...
Jason Rute's user avatar
  • 8,960
3 votes

Tutorial implementations of NbE

Does code in paper format count? In which case I would throw in Danvy, Keller, and Puech's Typeful Normalization by Evaluation You get an intro to deep vs. shallow, an analogy with printf, and an ...
gallais's user avatar
  • 1,256
2 votes

What are some good resources for Proof Assistant based exercises/puzzles for recreation and practice?

You already mention two very complete sites of exercises and I don’t have much reason to think there are more of that kind. In particular, Proving For Fun hosts the proving competition Proof Ground ...
Jason Rute's user avatar
  • 8,960
1 vote

Why use records for non-empty lists rather than inductively defined non-empty lists?

You could also try to use dependently typed sequences (I'm using the Mathematical Components library here), as in: ...
Pierre Jouvelot's user avatar
1 vote

How to deal with Binders?

This is kind of silly but I haven't really seen it concretely written down anywhere. Given a system of first-order logic you don't need to have a concrete system of terms at all but can only use ...
Ms. Molly Stewart-Gallus's user avatar

Only top scored, non community-wiki answers of a minimum length are eligible