Questions tagged [recommendations]

Use this for questions seeking an asset that give nebulous criteria rather than concrete specifics. If seeking literature such as books or papers use [tag:reference-request]. If seeking software use [tag:software-request].

Filter by
Sorted by
Tagged with
4 votes
3 answers
104 views

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

I've come across two main ways to do non-empty lists: ...
user avatar
  • 141
6 votes
1 answer
129 views

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

Proof Assistant based exercises and puzzles make for a good recreational activity, as well as help sharpen skills of users of said systems. There are many such equivalent resources for algorithmic ...
user avatar
8 votes
1 answer
160 views

How to deal with the proliferation of encodings of ASTs?

When working with type theory and ASTs one often ends up with a large amount of different encodings. It's very similar to the same problem in compiler design but more annoying because it's dependently ...
user avatar
16 votes
1 answer
305 views

Formalizations of unsolved problems

Is there a library (for any proof assistant) which provides formalized definitions of unsolved problems? To clarify, I mean some collection that correctly defines unsolved problems in the language of ...
user avatar
  • 509
13 votes
2 answers
443 views

Tutorial implementations of NbE

For a project I'm planning on doing with some students this summer, I'm looking for an implementation of normalization-by-evaluation whose code the students can read, understand, and extend. So I'd ...
user avatar
  • 2,127
7 votes
1 answer
236 views

Type Theory research groups

Research about type theory, internal languages, intuitionism, constructivism, and proof assistants is, at the moment, not as fashionable as other branches of mathematics are, say for example algebraic ...
user avatar
  • 508
12 votes
2 answers
139 views

verifying combinatorial constructions - choice of a proof assistant

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 ...
user avatar
13 votes
4 answers
164 views

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

I'm a theoretical computer scientist and my research is focused mainly on structural and algorithmic graph theory. Recently I've been very interested in using proof assistants. As a "pet project&...
user avatar
5 votes
1 answer
61 views

General Guidelines and Tips for using Induction

There are many kinds of induction (induction over the natural numbers ⊂ structural induction ⊂ Noetherian induction), when do I use which flavour? And what should I keep in mind when doing proofs by ...
user avatar
  • 998
3 votes
1 answer
154 views

How could I make a Proof Assistant? [closed]

If, as a complete beginner, I wanted to create a proof assistant, how would I begin to start this? How easy is one to create? What advice do you have? Note: contains "multiple questions" as ...
user avatar
  • 1,258
18 votes
2 answers
316 views

How to deal with Binders?

When reasoning about programming languages in a deep embedding, $\alpha$-equivalence, binders and capture-avoiding substitution quickly can become tedious. Complex binders may introduce multiple bound ...
user avatar
  • 998
10 votes
1 answer
83 views

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

As mentioned in another question, the way that VSCode and other editors implement unicode characters that cannot be typed directly from most keyboards is an editor feature. As such, different editors ...
user avatar