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].
14
questions
1
vote
0
answers
58
views
Embedding proof assistance in an application
Context
Perhaps this is too open-ended a question for StackExchange, in which case I apologize, but otherwise here goes:
I have a project I'm toying around with, the core of which is what I'd call &...
- 111
2
votes
0
answers
52
views
Tool for typing mathematical physics, e.g. differential geometry
Many expressions in mathematical physics use a rather sloppy notation, e.g. the Lie bracket on a vector field is defined using ambiguous notation, where $X : M \rightarrow TM$ is first defined as a ...
- 21
4
votes
3
answers
162
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:
...
- 141
6
votes
1
answer
191
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 ...
- 1,241
8
votes
1
answer
173
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 ...
- 2,768
16
votes
1
answer
325
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 ...
- 519
13
votes
2
answers
521
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 ...
- 2,912
9
votes
1
answer
292
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 ...
- 722
13
votes
2
answers
177
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 ...
- 480
14
votes
4
answers
226
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&...
- 143
5
votes
1
answer
78
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 ...
- 1,098
3
votes
1
answer
209
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 ...
- 1,308
17
votes
2
answers
373
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 ...
- 1,098
11
votes
1
answer
117
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 ...
