Why scientists don't write formal proofs

[Ivan Kuckir]

Today, many matemathicians come up with informal proofs of different theorems.

Usually, we have to wait several days / weeks / months, until these proofs are reviewed by other scientists and see, if abybody finds any error. Not many people understand such proof and errors can be found years later.

Would it be that hard to make mathematicians start writing formal proofs? I see, that a complex proof can have hundreds of thousands of lines in total. But since we already have theorem databases, writing a proof would mean just connecting existing bits (theorems) into a new bit. The "skeleton" of a new proof would not be so complex. And, of course, such proof can be checked instantly with a computer.

For example, there are about 100 papers claiming that they have solved the P vs NP problem (computational complexity theory). Most of them are not trusted, but also, most of them have not been thoroughly analyzed. Formal versions of proofs would remove all these confusions. Also, it would help govermnemns to decide, which scientist / institution should get the money, so investments into pseudo-science could be prevented.

So are you aware of any movement, which tries to make formal proofs the "default"? Or credibility of informal proofs is not as big problem as I think it is?

[Burton Samograd]

Is the job of mechanical translation as calling as the writing of the proof? Could one not just OCR the Principia and be done with it? I have a feeling the metamath 100 is not filling up with transcribers but people writing new work of old proofs using the new system. Some day transcription to systems like metamath will be a calling for these old analog works, much like programming is the transcription of mathematics.

Samograd

Sent with Unibox

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To post to this group, send email to meta...@googlegroups.com.
Visit this group at https://groups.google.com/group/metamath.
For more options, visit https://groups.google.com/d/optout.

[vvs]

On Tuesday, August 15, 2017 at 2:09:02 AM UTC+3, Ivan Kuckir wrote:

Would it be that hard to make mathematicians start writing formal proofs?

I doubt that. Some philosophers claim that symbolic logic is just about reducing complex real substance to a few artificial rules. They say that by defining senseless rules you could produce perfectly valid but senseless propositions. Thus formal verification just confirms that the rules are followed, but not that they actually make any sense. In their view translating real mathematics into formal logical description has little value. They view it only as a reductionistic attempt to derive all of the mathematics from just a single foundation, which is impossible by Gödel's incompleteness theorem. They are perfectly happy with informal proofs because they don't believe that symbolic logic has any real advantage for human reasoning. And that translating already existing informal proofs into formal language for no actual gain makes no sense for them.

This view has its merits, so it depends on the actual philosophy of the researcher. Personally, I found that using formal logic is very convenient for transcription of an existing work in a common language. It makes it more unambiguous for everyone and helps to reduce possible mistakes. But not every mathematician cares for that. They are trained to make and understand informal proofs and to be very proficient in it. So, formal logic shares the same fate as Esperanto.

[Jonathan Yan]

Symbolic logic gives math a mechanical foundation, a set of well-designed, objective rules of a difficult game. Mathematicians' understandings are useful internal models for them to navigate these rules and discover interesting patterns, but it's far from clear that their mathematical sense is the best internal model to play this mechanical game. It's possible that some alternative math semantics, very different from human intuition, can be highly effective at playing this game. Just like AlphaGo is highly effective at playing Go. Formal proofs are how these alternative methods can be researched, tested, then verified to have mathematical value at mechanical level.

--

You received this message because you are subscribed to the Google Groups "Metamath" group.

To unsubscribe from this group and stop receiving emails from it, send an email to metamath+unsubscribe@googlegroups.com.

[vvs]

On Tuesday, August 15, 2017 at 9:58:11 AM UTC+3, vvs wrote:

This view has its merits, so it depends on the actual philosophy of the researcher. Personally, I found that using formal logic is very convenient for transcription of an existing work in a common language. It makes it more unambiguous for everyone and helps to reduce possible mistakes.

I forgot to mention one important use case. Presently, there is no other way to help automate reasoning except to translate it to formal language. There are attempts to use natural languages for programming, but it has many implications.

[vvs]

On Tuesday, August 15, 2017 at 10:57:25 AM UTC+3, Jonathan Yan wrote:

Mathematicians' understandings are useful internal models for them to navigate these rules and discover interesting patterns, but it's far from clear that their mathematical sense is the best internal model to play this mechanical game. It's possible that some alternative math semantics, very different from human intuition, can be highly effective at playing this game.

Again, that depends on philosophy. Some would argue that there is no another sense outside human reasoning. So, it again reduce to the question: are different encodings of semantic models in syntactic rules gives us anything new? Or is it just a tautology?

[Jonathan Yan]

On Tue, Aug 15, 2017 at 4:09 PM, vvs <vvs...@gmail.com> wrote:

Again, that depends on philosophy. Some would argue that there is no another sense outside human reasoning. So, it again reduce to the question: are different encodings of semantic models in syntactic rules gives us anything new? Or is it just a tautology?-- 

Some might argue that there is no other form of reasoning, but that argument falls apart when we develop a system that uses its own semantics to find mechanical proofs which previously eluded the best efforts from mathematicians. Such a demonstration would not only be new, but have profound implications in the philosophical understanding of math, reasoning, and intelligence.

[Mario Carneiro]

On Tue, Aug 15, 2017 at 4:09 AM, vvs <vvs...@gmail.com> wrote:

On Tuesday, August 15, 2017 at 10:57:25 AM UTC+3, Jonathan Yan wrote:

Mathematicians' understandings are useful internal models for them to navigate these rules and discover interesting patterns, but it's far from clear that their mathematical sense is the best internal model to play this mechanical game. It's possible that some alternative math semantics, very different from human intuition, can be highly effective at playing this game.

Again, that depends on philosophy. Some would argue that there is no another sense outside human reasoning.

This seems to take it a bit too far. Even granting that human reasoning is the only one with "sense" (which I find dubious to begin with), it may be the case that some symbolic representation is more efficient at giving us the results we want in human terms than human reasoning itself. That is, the theorems that humans find interesting may be more efficiently provable by non-human methods, and there is no a priori reason to believe that just because the ends are human so too must the means be human. And indeed there are plenty of examples coming out of the formal mathematics community which show this "alien reasoning" (to quote Marijn Heule regarding the 200TB alien proof of the Boolean Pythagorean triples problem).
 

Mario

[vvs]

On Tuesday, August 15, 2017 at 11:18:23 AM UTC+3, Mario Carneiro wrote:

human so too must the means be human. And indeed there are plenty of examples coming out of the formal mathematics community which show this "alien reasoning" (to quote Marijn Heule regarding the 200TB alien proof of the Boolean Pythagorean triples problem).

But is it really "alien reasoning"? We can't think outside of our brain, so any reasoning that we could understand should be related to our semantics somehow. Also, any reasoning system created by humans should use reasoning that's originated from human reasoning. How much it evolved by itself? Could we call it artificial intelligence? And if not, what is an intelligence at all?

I find these questions tough. So, I'd say that I found formal logic practically useful, but I wouldn't dare to go further. And wouldn't blame those mathematicians who ignore formal logic and depend on informal proofs. That's the sole point of my arguments.

[vvs]

On Tuesday, August 15, 2017 at 11:18:23 AM UTC+3, Mario Carneiro wrote:

we want in human terms than human reasoning itself. That is, the theorems that humans find interesting may be more efficiently provable by non-human methods, and there is no a priori reason to believe that just because the ends are human so too must the means be human.

BTW, if I didn't make this clear, using the raw computing power to search for unknown tautologies is the reason why I find formal logic practically useful. But I don't believe that computers use alien reasoning, they are just faster and have more memory.

[fl]

> Some philosophers claim that symbolic logic is just about reducing complex real substance to a few artificial rules.

Sounds like a thesis about human language.
 

They say that by defining senseless rules you could produce perfectly valid but senseless propositions.

Philosophy and mathematics require to define terms before using them. What does "sense" mean?

 
> They view it only as a reductionistic attempt to derive all of the mathematics from just a single foundation, which is impossible by Gödel's incompleteness theorem.

Maybe but the theorems you have succeeded in proving are useful.
 

They are perfectly happy with informal proofs because they don't believe that symbolic logic has any real advantage for human reasoning. And that translating already existing informal proofs into formal language for no actual gain makes no sense for them.

This view has its merits, so it depends on the actual philosophy of the researcher.

Is truth that depends on the personnality of a subject a truth?

 

Personally, I found that using formal logic is very convenient for transcription of an existing work in a common language.

That was Leibniz's view too. By the way he died alone and sharply hated by Newton and his followers. There was nobody at his
burial but his servant. Scientists are cruel people.

But Newton was a virgin when he died. It's a consolation.

--
FL

[vvs]

On Tuesday, August 15, 2017 at 12:39:21 PM UTC+3, fl wrote:

> Some philosophers claim that symbolic logic is just about reducing complex real substance to a few artificial rules.

Sounds like a thesis about human language.

You're right, it is. That whole argument can be viewed at least from two points. The first is that some languages are better than others for certain purposes. That's my point of view.  The second is that by using a different language one can obtain some different reasoning somehow. I wouldn't subscribe to that view. By using different programming languages you can't claim that computers can "reason" about anything at all.

Maybe but the theorems you have succeeded in proving are useful.

True. But many mathematicians can prove theorems in natural language better that using formal logic. So, it has no value for them.

Is truth that depends on the personnality of a subject a truth?

Right, what is the "truth"? Some would argue that it depends on the agreement.

>What does "sense" mean?

In the same sense. It depends on understanding, so it isn't abstract or objective.

That was Leibniz's view too.

There were no computers in his times. So, he couldn't predict other practical use.

Scientists are cruel people.

Nope. They are just people. And no better than everyone else.

[Jonathan Yan]

On Tue, Aug 15, 2017 at 5:39 PM, 'fl' via Metamath <meta...@googlegroups.com> wrote:

Personally, I found that using formal logic is very convenient for transcription of an existing work in a common language.

That was Leibniz's view too. By the way he died alone and sharply hated by Newton and his followers. There was nobody at his
burial but his servant. Scientists are cruel people.

I can imagine why some mathematicians won't appreciate attempts at building alternative semantic models of math that can potentially be highly effective at theorem proving. After all, many mathematicians went through great length to build an effective math model in their brains, often at the cost of losing other useful abilities. Those models will be less valuable if they turn out to be not as effective as a model learned automatically by a computer.

[fl]

 

I can imagine why some mathematicians won't appreciate attempts at building alternative semantic models of math that can potentially be highly effective at theorem proving. After all, many mathematicians went through great length to build an effective math model in their brains, often at the cost of losing other useful abilities. Those models will be less valuable if they turn out to be not as effective as a model learned automatically by a computer.

With transhumanism they will all lose their jobs you mean? Possibly. Terrifying no?

Google is the friend of nobody.

-- 

FL

[vvs]

On Tuesday, August 15, 2017 at 1:12:21 PM UTC+3, Jonathan Yan wrote:

I can imagine why some mathematicians won't appreciate attempts at building alternative semantic models of math that can potentially be highly effective at theorem proving. After all, many mathematicians went through great length to build an effective math model in their brains, often at the cost of losing other useful abilities. Those models will be less valuable if they turn out to be not as effective as a model learned automatically by a computer.

Absolutely. If you are a famous poet, writing in a foreign language makes you just an average graphomaniac. There will be a translation layer which makes your efforts less effective. That means that to be effective, mathematicians should learn formal logic at school and build further from that base.

But I don't think that anyone takes computers seriously as a replacement for a proficient mathematician. Though, chess was out of reach some time ago, but everything changes. Still, I don't believe that computers could do anything more that just a good tool does. If computers indeed could prove any theorems, that would be a cause to call it an artificial intelligence. And that would be a frightening development for many. Personally, I wouldn't want computers to be anything more than just a good tool. I wouldn't want computer Spartacus to take my way of life.

[David A. Wheeler]

On August 14, 2017 7:09:02 PM EDT, Ivan Kuckir <ivan....@gmail.com> wrote:
>Today, many matemathicians come up with informal proofs of different
>theorems.
>
>Usually, we have to wait several days / weeks / months, until these
>proofs
>are reviewed by other scientists and see, if abybody finds any error.
>Not
>many people understand such proof and errors can be found years later.
>
>Would it be that hard to make mathematicians start writing formal
>proofs?

...

>So are you aware of any movement, which tries to make formal proofs the
>"default"? Or credibility of informal proofs is not as big problem as I
>think it is?

There is such a movement, any of the people participating in any of the formal methods systems are at least in some sense part of that. Freek, for example, has long been advocating for this.

There are at least two problems: (1) convincing people that it is practical and (2) hubris.

Historically the big problem with formal mathematics systems is that it is much more difficult to create formal proofs than informal proofs. That matters a lot to many mathematicians, since anything that makes things too difficult to publish will inhibit their ability to get tenure or other goodies. The continuing work to create proofs in metamath and other systems, as well as tools to help them, has been a gradual process of making it easier. Imagine trying to pray proofs and metamath in 1996, where a lot of the tools and proofs we use now were unavailable. There is reason to hope that over time it will slowly get easier and easier, not easy but easier.

Hubris is the bigger problem. Mathematicians freely admit that other mathematicians make mistakes, and they might be willing to admit that they might make a mistake. But many act in practice as if they never make mistakes, or that it doesn't matter if they do, because many are not interested in tools that can automatically check their work. Of course, it doesn't matter if math is just a game that you play. But mathematics is more than a game. Science and technology build upon mathematics, even in cases where people regionally thought it was just abstract mathematics with no applications. I would like to see mathematics built on much stronger and much more rigorously verified foundations, and I think that formal verification is a critical part of that.



--- David A.Wheeler

[vvs]

On Tuesday, August 15, 2017 at 3:35:50 PM UTC+3, David A. Wheeler wrote:

Hubris is the bigger problem. Mathematicians freely admit that other mathematicians make mistakes, and they might be willing to admit that they might make a mistake. But many act in practice as if they never make mistakes, or that it doesn't matter if they do, because many are not interested in tools that can automatically check their work.  Of course, it doesn't matter if math is just a game that you play. But mathematics is more than a game. Science and technology build upon mathematics, even in cases where people regionally thought it was just abstract mathematics with no applications.  I would like to see mathematics built on much stronger and much more rigorously verified foundations, and I think that formal verification is a critical part of that.

Sure. I've seen many notable mathematicians claiming that making a mistake is not crucial, because it will be found and fixed anyway. Calculus, Russel paradox and ZFC are taken as an example of that. That's how mathematics evolved over time. If I'm not mistaken, Hilary Putnam advocated that mathematics doesn't need foundations at all.

[vvs]

On Tuesday, August 15, 2017 at 3:35:50 PM UTC+3, David A. Wheeler wrote:

it doesn't matter if math is just a game that you play. But mathematics is more than a game. Science and technology build upon mathematics, even in cases where people regionally thought it was just abstract mathematics with no applications.

And I couldn't resist not to mention G.H.Hardy, who always spread the views that mathematics is just a useless game.

[fl]

 

But I don't think that anyone takes computers seriously as a replacement for a proficient mathematician.

Yes they do. The enemy of capitalism is work. It is structural. But in fact I don't think it is a terrible thing if human beings are replaced by humanoids. Because with the millions of tons of

radioactive nuclear waste spread throughout the whole world we have been producing and we are not able to manage I just wonder who could survive but a machine.

-- 

FL

[vvs]

On Tuesday, August 15, 2017 at 9:44:21 PM UTC+3, fl wrote:

beings are replaced by humanoids. Because with the millions of tons of

radioactive nuclear waste spread throughout the whole world we have been producing and we are not able to manage I just wonder who could survive but a machine.

Well, I can't survive in a machine world, so I don't care about machines. Am I egoist? Yes. Am I a social being? Yes, but only if it's a human society. So, I care for humans as a whole to support my egoistic life. Well, I suppose I could even sacrifice myself for human cause, because I can't live without humanity anyway and out of gratitude. Some humans (but not all of them) made my life better than it could be, but would machines do that for me too? I doubt that.

Seriously, I'd love to express my gratitude in some constructive way, e.g. making the life of other humans better. Learning and working are the best ways to do it. Mathematics has a good potential, because as David put it: it's not a game. Some mathematicians just think differently.

[fl]

Seriously, I'd love to express my gratitude in some constructive way, e.g. making the life of other humans better.

Send a curriculum vitae to Google?

 

-- 

FL

[vvs]

On Tuesday, August 15, 2017 at 10:05:53 PM UTC+3, fl wrote:

Seriously, I'd love to express my gratitude in some constructive way, e.g. making the life of other humans better.

Send a curriculum vitae to Google?

Why? Don't you believe in your own abilities? Google isn't good or evil - it's just not human. And it doesn't understand human sarcasm.

The fact is - there is no mathematics (or Google) per se, everything is a product of human activities. So, formal logic doesn't do reasoning - you do. But you might use or not use it - that's your ability as a human. Perhaps, machines could do that too, but that's just a presumption, not a fact. And any hypothesis should be proved.

I believe that humans should support their society and society should support them. That's just a reasonable thing to do for all humans to survive. If humans can't think reasonably, then I suppose we all doomed. But that a presumption, which should be proved or disproved first. Everyone could do at least something. Like we can't make all mathematicians to use formal logic, but we can improve it and hope for success. We could then say, that at least we tried.

[fl]

 

Why? Don't you believe in your own abilities? Google isn't good or evil - it's just not human. And it doesn't understand human sarcasm.

Amateur of positive thinking. I see. Google will appreciate.

 

The fact is - there is no mathematics (or Google) per se, everything is a product of human activities. So, formal logic doesn't do reasoning - you do. But you might use or not use it - that's your ability as a human. Perhaps, machines could do that too, but that's just a presumption, not a fact. And any hypothesis should be proved.

There are good evidences nowadays that a human being is a carbon-based, auto-replicating, Darwinian machine that sustained itself with

a catabolism fed by a food chain with chlorophill at its base.

But we can replace it by a silicium-based machine whose energy is supplied by uranium fission. A matter of technology choice that's

all. 

And to have a mathematician: a good database, some AI, a minmax algorithm (ok something a bit more

sophisticated; it's just to give an idea),  a clock with a pretty good frequency, a good parser and a good semantics

 and it's ok.

Do you believe in Darwinism?

--

FL

[Ken Kubota]

Actually, some mathematicians do provide formal proofs.

One prominent example is Peter B. Andrews with his 2002 textbook (ISBN 1-4020-0763-9).

I was able to implement most proofs in it more or less exactly as presented by Andrews

in my R0 software implemention, see http://www.owlofminerva.net/files/formulae.pdf

or http://doi.org/10.4444/100.3.

However, formalizing even simple proofs is a lot of work, and for this reason many

mathematicians prefer providing informal proofs only, although I believe that they mentally

use the same rules (mechanisms) of inference as in formal (symbolic) logic.

It should be noted that besides the semantic approach, where meaning is obtained by some

metatheory, there is also the syntactic approach which considers the (few) syntactical

rules of inference as philosophically justified, and therefore the attempt to reduce mathematics

to formal logic as very important. Russell’s attempt of reducing mathematics to formal logic

and Andrews' notion of expressiveness are of the same spirit, which is the reason for why

I also use the term reducibility instead of expressiveness.

Moreover, for the syntactic approach, Gödel’s theorem is philosophically irrelevant.

For it, the theorem only states that there are well-formed formulae which cannot be

inferred (or refuted), but since meaning is not derived from a metatheory, there is

no gap between syntax and semantics, hence there is no incompleteness

(because not every well-formed formula is expected to be meaningful per se).

With the syntactic approach, completeness directly follows from the fact that

meaning (semantics) is identical with syntax (formal/syntactical inference).

In the computer era, formalization and formal logic in practical applications have 

become as important as in philosophy in former times. It is already used

for safety critical applications such as aviation, and I would also expect an

increasing demand in the developing field of automated car navigation.

____________________________________________________

Ken Kubota

http://doi.org/10.4444/100

--
You received this message because you are subscribed to the Google Groups "Metamath" group.

To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.

[fl]

There are good evidences nowadays that a human being is a carbon-based, auto-replicating, Darwinian machine that sustained itself with

a catabolism fed by a food chain with chlorophill at its base.

But we can replace it by a silicium-based machine whose energy is supplied by uranium fission. A matter of technology choice that's

all. 

We might even call it a choice of civilization, I dare say. But Google will not hesitate in my opinion.

 

--

FL

[Giovanni Mascellani]

Hi,

Il 15/08/2017 14:35, David A. Wheeler ha scritto:
> There is such a movement, any of the people participating in any of
> the formal methods systems are at least in some sense part of that.
> Freek, for example, has long been advocating for this.
>
> There are at least two problems: (1) convincing people that it is
> practical and (2) hubris.
>
> Historically the big problem with formal mathematics systems is that
> it is much more difficult to create formal proofs than informal
> proofs. That matters a lot to many mathematicians, since anything
> that makes things too difficult to publish will inhibit their ability
> to get tenure or other goodies. The continuing work to create proofs
> in metamath and other systems, as well as tools to help them, has
> been a gradual process of making it easier. Imagine trying to pray
> proofs and metamath in 1996, where a lot of the tools and proofs we
> use now were unavailable. There is reason to hope that over time it
> will slowly get easier and easier, not easy but easier.

I think this point can hardly be understressed. I am not a power
Metamath user, but when I tried it took me many hours to encode a single
"one can easily see that..." point (and it was really trivial!). There
is really a lot of implicit work under all the informal proofs that
mathematicians usually produce, many orders of magnitude. I personally
think that the routine formalization of research level maths will be
eventually possible, but we really need to achieve an impressive cut in
writing time. I would like to test whether machine learning, which made
miracles in many fields, can do something here, but have no idea of when
I will have time to test.

Another way to express the difficulty of formalizing maths is to see how
much of it has actually been formalized: a lot of great people worked on
the Metamath set.mm, but, except in a few areas, the things in there
hardly reach the third undergraduate year (speaking in the Italian
perspective, at least). As an example (relevant from my point of view of
a differential geometer), both integration and differentiation theory
are just hinted, only in the special case of R. It is clearly
impossible, at this point, to formalize my current research work.

> Hubris is the bigger problem. Mathematicians freely admit that other
> mathematicians make mistakes, and they might be willing to admit that
> they might make a mistake. But many act in practice as if they never
> make mistakes, or that it doesn't matter if they do, because many are
> not interested in tools that can automatically check their work. Of
> course, it doesn't matter if math is just a game that you play. But
> mathematics is more than a game. Science and technology build upon
> mathematics, even in cases where people regionally thought it was
> just abstract mathematics with no applications. I would like to see
> mathematics built on much stronger and much more rigorously verified
> foundations, and I think that formal verification is a critical part
> of that.

Actually, there are many fields in which formal proving is at least
partially used to ensure safety and functionality. These fields tend to
be closer to computer science and programming than what is commonly
known as mathematics (usually I consider most of computer science a
branch of mathematics, but I think it is better to retain the
distinction here). In the case of "abstract" mathematics, the pressure
to formalization is probably much less. However, personally I would be
interested in knowing whether my PhD thesis is correct or not: I really
hope it is and I put every effort I could to make sure it was, but as I
mentioned above at the moment there is no way I can formalize it in
reasonable time (even less so considering that I would have to formalize
all its dependencies first).

I really hope to see the day in which formalizing a theorem is not much
longer than (properly) writing it in LaTeX.

My 2 cents, Giovanni.
--
Giovanni Mascellani <g.masc...@gmail.com>
PhD Student - Scuola Normale Superiore, Pisa, Italy

http://poisson.phc.unipi.it/~mascellani

[fl]

 As an example (relevant from my point of view of
a differential geometer), both integration and differentiation theory
are just hinted, only in the special case of R. It is clearly
impossible, at this point, to formalize my current research work.

Sure the Laplacian and the Riemannian manifold are missing.

--

FL 

[Shawn Wang]

Another part of mathematics that is completely missing in Metamath is differential equations, or any other branches that involve symbolic or numerical calculations. Though in the Metamath textbook the author made a distinction between systems that do formalized reasoning (e.g. Metamath) and systems that do symbolic algebra (e.g. Mathematica), in order to popularize an automated theorem prover to the mass mathematicians, it has to incorporate some calculative aspect.

I speculate that when formalized reasoning and contemporary mathematics finally work in harmony, it is not because mathematicians all start to write formalized mathematics. There should be a system that can automatically transfer what is written in prose into formalized mathematics, making Bourbaki's "theoretically formalizable" claim possible. Everything should be done transparently.

[David A. Wheeler]

> > As an example (relevant from my point of view of
> > a differential geometer), both integration and differentiation theory
> > are just hinted, only in the special case of R. It is clearly
> > impossible, at this point, to formalize my current research work.

It's not *impossible* - the problem is that many other lower-level constructs need to be formalized first.

The only way to solve this, I think, is to continue the work of formalizing lower-level constructs. As constructs are added, whole new areas become practical. Another area that's clearly lacking in Metamath are agreed-on ways to handle geometry, including Euclidean geometry (see: https://github.com/metamath/set.mm/issues/49 ). The bad news is that it's work, the good news is that every step opens new vistas.

MPE is absolutely *not* just a optical-reader-copy of Principia Mathematica (PM). PM's approach to sets is *not* how most people approach sets (most use ZFC), and in any case, MPE goes *way* beyond PM in terms of what it proves. It took until PM's volume 2 to get to "1+1=2"; MPE goes far beyond *that*.

--- David A. Wheeler

[fl]

 

Another area that's clearly lacking in Metamath are agreed-on ways to handle geometry, including Euclidean geometry (see: https://github.com/metamath/set.mm/issues/49 ).

We have already spoken of that David. I just don't remember in what post.

But euclidean geometry is already present in metamath in the three ways we meet

it in literature.

--

FL

[Giovanni Mascellani]

Il 17/08/2017 23:39, David A. Wheeler ha scritto:
> It's not *impossible* - the problem is that many other lower-level
> constructs need to be formalized first.

That is what I meant: it is practically impossible to do it in the near
future.

> The only way to solve this, I think, is to continue the work of
> formalizing lower-level constructs.

I fully agree on this; also, I think that the process will become much
easier while better tool for producing Metamath proofs are written.

[fl]

I fully agree on this; also, I think that the process will become much
easier while better tool for producing Metamath proofs are written.

The Tools are good. Believe me. I know what I'm speaking of.

 

--

FL