robinzfc

7 ms·

31.
by robinzfc 3y ago
Right. Specifically, the codomain needs to be an abelian group. And even that is not sufficient as one needs also an action of the field of scalars on that codomain with the right properties.
32.
by robinzfc 4y ago
This is a weird article. It uses the expressions like "iron fist" and "mandated", but when you follow the links provided as sources all you get is "the bank wanted 60% of its people back in the office, but was only
33.
by robinzfc 4y ago
Many years ago I was working on a device driver for a position sensor. After deployment the customer complained that every time they started another process on the monitoring machine where the driver was installed the position sensor readin
34.
by robinzfc 4y ago
> except serve as a basis for practical formalization of proofs I do formalized mathematics as a hobby and I can not see any basis for that opinion. Freek Wiedijk wrote an interesting paper [0] where he compared the complexity of various
35.
by robinzfc 4y ago
I think it is interesting to compare this to the previous attempt from 2013 by Gowers (and Mohan Ganesalingam) described in a blog series ending with https://gowers.wordpress.com/2013/04/14/answers-results-of-
36.
by robinzfc 5y ago
I am a software engineer with education in mathematics and I have been working on a formalized mathematics project for the last 16 years (on and off). There is no particular purpose of this, other than it is a good mental workout and a sati
37.
by robinzfc 5y ago
This is very similar to Isabelle's Isar [1], except that Isar definitions and theorems can be formally verified. MMathLingua has no doubt a much better presentation layer for mathematics than Isabelle/Isar. This can be improved w
38.
by robinzfc 5y ago
It depends on what you mean by "fully featured" but Isabelle supports ZF logic [1] and also you can do ZFC in Isabelle/HOL [2]. And, of course there is Mizar [3]. [1] https://isabelle.in.tum.de/dist/libra
39.
by robinzfc 6y ago
> If not proof trees, what? Just make the proof language similar to the standard mathematics language and possibly process it with a presentation layer that makes it even better. The examples start from Mizar [1] (since 1973), IsarMathL
40.
by robinzfc 6y ago
The current tittle of the original MathOverflow question is "What makes dependent type theory more suitable than set theory for proof assistants?", I don't know why is it different than here. The actual question makes more se
41.
by robinzfc 6y ago
> lower per capita death rate than the best EU member states (Germany, Denmark). You repeat that a couple of times in your posts, I am curious where do you get that from? Germany and Denmark are not "the best", they are both ab
42.
by robinzfc 7y ago
The construction of real numbers does not need the axiom of choice in the sense that there are constructions of models of real numbers that do not need it. One example of such construction is described on the Wikipedia page [1], look for &q
43.
by robinzfc 7y ago
What logicchains says above is true in some sense but of course it depends on the degree of automation a given theorem proving environment provides. In Isabelle a proof may consist of the keyword "using" followed by a list o 9-10
44.
by robinzfc 7y ago
Isabelle allows the user to define symbols. So, those two operations are represented by different symbols in the source (the *.thy files) but the presentation layer renders them both as "+". You may want to look at the correspondi
45.
by robinzfc 7y ago
It is not difficult to keep the notation sane in formalizations based on set theory. One way is to defer overloading of symbols to the presentation layer. You can see an example of that at [1] where the + sign is used to denote the group op