bio  website  andrej.com 

location  Ljubljana  
age  44  
visits  member for  5 years, 9 months 
seen  22 hours ago  
stats  profile views  7,724 
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 nonconstancy in constructive analysis
It's not very complicated. I could prove that $f$ is locally nonconstant 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 nonconstancy in constructive analysis
No, I do not because you could prove nonconstancy 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 nonconstancy in constructive analysis
It's a legitimate question, but it's not researchlevel. It's an exercise in fiddling with numbers. 
Jul 28 
comment 
(Reference request) Unwinding the notion of local nonconstancy 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 nonconstancy 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 nonconstant 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 nonconstant under certain conditions. 
Jul 21 
comment 
Elementary treatment of elementary functions in constructive math
You don't need nonconstancy 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? 