19,455 reputation
348113
bio website andrej.com
location Ljubljana
age 44
visits member for 5 years, 9 months
seen 22 hours ago
I am a professional mathematician. My area of research is logic, constructive and computable mathematics, category theory, and semantics of programming languages.

1d
comment Detecting positive endomaps of the formal reals
How do you extend the map $f$ from reals to the locale of reals? Or this something that Erik does?
2d
comment (Reference request) Unwinding the notion of local non-constancy in constructive analysis
It's not very complicated. I could prove that $f$ is locally non-constant by applying some lemma, thereby not giving explicit witnesses. You would have to "unwind" my proof (normalize it) to figure out what the witness actually is. There is an important theorem about intuitionistic logic, namely the disjunction and existence property. It says that every proof of an existential statement allows us to extract an explicit witness, but the procedure for doing so is complicated (it requires normalization which converts the proof into a special normal form).
2d
comment (Reference request) Unwinding the notion of local non-constancy in constructive analysis
No, I do not because you could prove non-constancy in some other way which provides a witness only after you normalize the proof.
2d
comment If wolfram rule 110 is universal , does it mean it can solve mathematical equations?
It means that you can write a program for solving mathematical equations (if you know how to), and then use Rule 110 to run your program.
Jul
28
comment (Reference request) Unwinding the notion of local non-constancy in constructive analysis
It's a legitimate question, but it's not research-level. It's an exercise in fiddling with numbers.
Jul
28
comment (Reference request) Unwinding the notion of local non-constancy in constructive analysis
It is not the case that in constructive analysis you have to bring everything down to Cauchy sequences and do everything at a pedestrian level. After establishing some basic properties of the exponential function, you can just argue the same was as @James does. If you want to see explicit witnesses, stick the proofs in a proof assistant and have it compute them for you. I repeat again that this problem is about explicit calculations and estimates, not about constructive mathematics.
Jul
26
comment (Reference request) Unwinding the notion of local non-constancy in constructive analysis
As I said in the other question, you are asking for nasty details and explicit manipulations of numerical approximations which are best done in the privacy of one's office. It would be difficult to find these to get published. I emphasize again that there is nothing particularly constructive about your question. You would hit exactly the same problem if you asked for explicit classical proofs. If you can show me explicit classical proofs I promise to translate it to a constructive ones. Let us start with the non-constant polynomials.
Jul
21
comment Elementary treatment of elementary functions in constructive math
Ok, looking at your example, this isn't really about constructive mathematics. You just want us to do the nasty details for you. You would have exactly the same kind of problem if you replaced "constructive" with "numeric" or "explicit" everywhere. As my professor of analysis said "you do it in the sweat of your face" (that's a Slovene expression).
Jul
21
comment Elementary treatment of elementary functions in constructive math
Since we seem to be using Cauchy reals it would be a good idea to have countable (or dependent) choice. Otherwise the Cauchy reals are not even Cauchy complete...
Jul
21
comment Elementary treatment of elementary functions in constructive math
Can you please explain why you want to do things this way? Are you teaching a course? Before we can answer your question you would have to explain precisely how you defined $\sin$, $\cos$, etc. I would recommend that instead you prove a general theorem about Taylor series being locally non-constant under certain conditions.
Jul
21
comment Elementary treatment of elementary functions in constructive math
You don't need non-constancy for Taylor's theorem.
Jul
20
comment Minimum regular open set containing a given set in a T0 Alexandrov topological space
When you say Alexandrov topological space, do you mean the topology on a poset that consists of the upper sets?
Jul
8
comment Does “$\forall Z(C(X,Z) \cong C(Y,Z))$” imply $X\cong Y$?
Aren't you close to establishing that the problem is undecidable by some cardinal arithmetic trouble?
Jul
7
revised What technical and/or theoretical challenges are involved in automatically extracting proofs from books and papers into Coq code?
deleted 9 characters in body
Jul
7
awarded  Nice Answer
Jul
7
comment What technical and/or theoretical challenges are involved in automatically extracting proofs from books and papers into Coq code?
I have asked people from Gonthier's team to write an answer. Let's hear it from the horse's mouth.
Jul
7
revised What technical and/or theoretical challenges are involved in automatically extracting proofs from books and papers into Coq code?
added 2381 characters in body
Jul
7
comment What technical and/or theoretical challenges are involved in automatically extracting proofs from books and papers into Coq code?
I see there is a lot of misunderstanding, I'll amend my answer to explain better what "implicit knowledge" is, and also address the feeling that formalization necessarily amounts to wasting time on details. Regarding the current state of tools and how cumbersome they are to use: my #1 suggestion for improvement was "better tools".
Jul
6
answered What technical and/or theoretical challenges are involved in automatically extracting proofs from books and papers into Coq code?
Jul
5
comment Subsequence and integers as a sum of $\frac{1}{n}$
Excuse the stupid question, but what if $M$ is negative?