Questions tagged [soft-question]

For questions whose answers can't be objectively evaluated as correct or incorrect, but which are still relevant to this site. Please be specific about what you are after.

Filter by
Sorted by
Tagged with
6 votes
4 answers
626 views

Inductive vs. recursive definitions

In Coq there are two ways to define a new type on an inductive type: Using Inductive and using Fixpoint. What are pros and cons ...
8bc3 457f's user avatar
  • 224
2 votes
0 answers
66 views

Formalization of Analytic Number Theory

Is there any formalization, in any proof checking environment (Lean, Isabelle, etc.) of basic analytic number theory, say everything in a book like the Titchmarsh book (The Theory of the Riemann Zeta ...
EGME's user avatar
  • 131
4 votes
1 answer
273 views

Why is it hard to formalize informal proofs?

Say I have some informal but rigorous argument in line with eg real analysis. Currently, it is a massive PITA to do algebraic manipulations in proof assistants like Coq or Isabelle. However, in ...
user2013's user avatar
15 votes
3 answers
264 views

Counterexamples in Type Theory

The title pretty much covers it. I'm wondering if someone is maintaining a list of counterexamples in type theory. I'm aware of Counterexamples in Type Systems, which I think is very nice, but I guess ...
Nathan's user avatar
  • 348
8 votes
2 answers
211 views

Figures on computer proof assistant usage

I'm interested in figures on computer proof assistant usage. To put this in perspective, I have a server which I am making at the moment, and I only feel like committing time to setting up four or ...
Cayley-Hamilton's user avatar
4 votes
1 answer
239 views

How can you represent a dependent type visually?

So, obviously for a term $t$ of type $T$, I would represent it as: T +-----------+ | | | t | | | +-----------+ That is a node ...
Daniel Donnelly's user avatar
4 votes
2 answers
146 views

Pragmatic encodings of inductive inductive types

What's the most pragmatic encoding for inductive-inductive types such as for a universe of types? In pseudo Coq syntax. ...
Molly Stewart-Gallus's user avatar
1 vote
1 answer
342 views

How does Lean4 (or a typical PA) represent lambda functions or in other words arbitrary expressions?

Question: Say I wanted my language to support various operator symbols, the semantics of which are defined by the user or by axioms. I'm wondering whether Lean4 (or a typical well-known PA) just ...
Daniel Donnelly's user avatar
-3 votes
1 answer
145 views

Could we speed up ATP or ATD using a directed graph that appears to work like a gigantic brain?

So I'm not sure how things are done in Lean4 or Coq, but I'm interested in their search features. For example, "Search for all theorems that get satisfied given a user-defined list of ...
Daniel Donnelly's user avatar
17 votes
2 answers
438 views

What are the advantages to impredicativity?

Mostly when I read about impredicativity I see people bemoaning its downsides. But it's not clear to me why I would want impredicativity in the first place. Impredicativity is useful for analyzing ...
Molly Stewart-Gallus's user avatar
12 votes
1 answer
243 views

Naming conventions (letter case, underscores, &c) for Coq

Does Coq have an established convention/style for constructors, variables, terms, &c? An established convention that isn't exceptionless is totally fine. For example, terms should be lowercase ...
Greg Nisbet's user avatar
  • 2,711
15 votes
1 answer
328 views

Why should you "never resort to polymorphism when initiality would do"?

In the concluding statement of "universe hierarchies", Conor McBride calls it [...] that key lesson which I learned from James McKinna: never resort to polymorphism when initiality will do. ...
James Martin's user avatar
  • 1,015
9 votes
2 answers
386 views

Which proof assistant would you advise me to learn (in 2022) considering my interests?

I am a math teacher in college. I’m very interested in type theory. So far, I got the general idea of it but I would like to go deeper. I am interested in philosophy of maths, in foundations of maths, ...
Colas's user avatar
  • 191