Questions tagged [mathematics]
Use this tag for questions a mathematician would feel at home answering and can be traced back to an area of mathematics.
22
questions
12
votes
3
answers
523
views
Why are impredicative constructions used less in type theory than in material set theory?
Many infinitary objects in (say) ZFC are constructed with impredicative principles. The natural numbers are formed by intersecting every inductive set (whose existence is given by the axiom of ...
- 4,025
12
votes
2
answers
123
views
Proof assistants with dynamic scope/local instances/etc.?
Say I'm formalizing something in group theory, and I'm working with some action $\cdot$ of $(G, +)$ on a set. In my math textbook, the identity of $\cdot$ is explicitly mentioned once (if that), and ...
- 221
8
votes
1
answer
153
views
What are some useful resources for a mathematician interested in learning Isabelle/HOL?
What are some useful and reliable resources for a mathematician interested in learning Isabelle/HOL? Could be online (websites) or physical (books).
- 1,338
8
votes
1
answer
127
views
Have the common algorithms in existing computer-assisted proofs been transitioned to proof assistants?
In my experience, one of the most common applications of computer-assisted proofs in math is establishing that a given system of constraints is infeasible. Here are some examples of settings and tools ...
- 981
5
votes
0
answers
1k
views
What's the general idea (intuition) behind Andrej's topos where reals are countable? [closed]
I am very surprised that Andrej Bauer claimed to have found a topos where reals are countable. He said it'll take a month to write down the proof, and I think that's very understandable.
However, I'm ...
- 6,316
2
votes
2
answers
206
views
What is known about minimal sets of axioms? [closed]
There are several axioms that are known to be independent of the usual ones; for instance, the Axiom of Choice. This axiom can be stated in several equivalent ways, e.g.:
For every set $A$, $\mathcal{...
- 495
2
votes
1
answer
54
views
Proving factors of GCD in Dafny
While trying to prove various properties of GCD I ran into a proof I am a bit stumped with. Gcd can be defined as the max element in the intersection of the divisors of two numbers. In the code I used ...
- 181