Search Results
| Search type | Search syntax |
|---|---|
| Tags | [tag] |
| Exact | "words here" |
| Author |
user:1234 user:me (yours) |
| Score |
score:3 (3+) score:0 (none) |
| Answers |
answers:3 (3+) answers:0 (none) isaccepted:yes hasaccepted:no inquestion:1234 |
| Views | views:250 |
| Code | code:"if (foo != bar)" |
| Sections |
title:apples body:"apples oranges" |
| URL | url:"*.example.com" |
| Saves | in:saves |
| Status |
closed:yes duplicate:no migrated:no wiki:no |
| Types |
is:question is:answer |
| Exclude |
-[tag] -apples |
| For more details on advanced search visit our help page | |
Results tagged with soft-question
Search options answers only
not deleted
user 1176
Questions that are about research in mathematics, or about the job of a research mathematician, without being mathematical problems or statements in the strictest sense. Do not use this tag for easy or supposedly easy mathematical questions.
233
votes
Accepted
What makes dependent type theory more suitable than set theory for proof assistants?
I apologize for writing a lengthy answer, but I get the feeling the discussions about foundations for formalized mathematics are often hindered by lack of information.
I have used proof assistants for …
- 48.8k
159
votes
How to present mathematics to non-mathematicians?
I have given talks about mathematics to non-mathematicians, for example to a bunch of marketing people. To see an example of a talk of mine that was given to a general audience, see my talk Zeros, giv …
76
votes
On proof-verification using Coq
Coq is a proof assistant, and not the only one. Other popular ones are Agda, Isabelle and the related HOL light. They all use type theory as a mathematical foundation (as opposed to first-order logic …
- 48.8k
45
votes
What are your favorite instructional counterexamples?
Counterexamples are very important when a student learns how to think in intuitionistic logic (and he has already been "spoiled" by classical logic). The counterexamples destroy the classical intuitio …
44
votes
Awfully sophisticated proof for simple facts
If two elements in a poset have the same lower bounds then they are equal by Yoneda lemma. (I actually said this in a seminar two weeks ago, and of course I explained I killed a mosquito with a nuke.) …
39
votes
Accepted
What is some current research going on in foundations about?
It is quite difficult to answer this question comprehensively. It's a bit like asking "so what's been going on in analysis lately?" It is probably best if logicians who work in various areas each answ …
37
votes
What are some ways to stay engaged with the mathematical community from outside academia?
If you like computers, you could consider getting into formalized mathematics, which is mathematics done completely formally and verified by computer programs, known as proof assistants. Formalized ma …
32
votes
Depressed graduate student.
I find it helpful to always work on more than one project at a time. When I get stuck, depressed, or disinterested with one task, I can always switch to another. I find that helpful. The projects ran …
30
votes
What does a theoretical mathematician do?
There are several things that mathematicians do:
teachers of mathematics teach math, and you surely know some of those,
applied mathematicians use their knowledge of mathematics to help engineers, p …
26
votes
What are some important but still unsolved problems in mathematical logic?
The modern logic (and foundational mathematics in general) of the 20th century gave us many important things: Russell's type theory, Zermelo-Fraenkel's set theory, meta-theorems about first order logi …
24
votes
Old books you would like to have reprinted with high-quality typesetting
Just for fun, Principia mathematica.
24
votes
Does the "propositions-as-types" paradigm match mathematical practice?
There are many aspects to the question "does a logical formalism reflect mathematical practice?" I will focus just on a very simple but important detail that every mathematician is familiar with.
In …
- 48.8k
23
votes
What technical and/or theoretical challenges are involved in automatically extracting proofs...
I am going to answer the question as if you asked about massive formalization of proofs, not automatic extraction of formal proofs from existing informal proofs written in books, because that's a fair …
23
votes
Locales and Topology.
I would recommend Peter Johnstone's "Stone Spaces", Cambridge University Press, 1982.
For a recent result see Alex Simpson's "Measure, Randomness and Sublocales". He shows that in locale theory it is …
23
votes
Mathematicians whose works were criticized by contemporaries but became widely accepted later
Brouwer's intuitionistic mathematics was heavily criticized by his contemporaries, most notably Hilbert. For almost a century it was casually ridiculed by mathematicians who had no clue whatsoever abo …