Skip to main content

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
3 votes
0 answers

Bounding Volume Proof Assistant Library

I am interested in learning Lean/Coq/Isabelle etc. and wanted to try to formalize Joseph O'Rourke's Minimum Bounding Box Algorithm. I do not have much experience with proof assistant tools. Is there a ...
WakkaTrout's user avatar
1 vote
0 answers

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 &...
Eric Anderson's user avatar
2 votes
0 answers

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 ...
user2361's user avatar
4 votes
3 answers

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: ...
nobody's user avatar
  • 141
6 votes
1 answer

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 ...
Agnishom Chattopadhyay's user avatar
8 votes
1 answer

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 ...
Ms. Molly Stewart-Gallus's user avatar
16 votes
1 answer

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 ...
Reubend's user avatar
  • 519
14 votes
2 answers

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 ...
Mike Shulman's user avatar
  • 3,070
9 votes
1 answer

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 ...
Nico's user avatar
  • 722
13 votes
2 answers

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 ...
Dima Pasechnik's user avatar
14 votes
4 answers

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&...
Rafael Coelho's user avatar
5 votes
1 answer

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 ...
Wno-all's user avatar
  • 1,108
3 votes
1 answer

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 ...
taylor.2317's user avatar
  • 1,318
17 votes
2 answers

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 ...
Wno-all's user avatar
  • 1,108
11 votes
1 answer

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 ...
Bjørn Kjos-Hanssen's user avatar