Hacker News Reader

Comment by michaelochurch | Hacker News Reader

I'm of the mind that there is immense value in being able to figure out difficult proofs.

Absolutely.

However, the rabbit hole is very deep. Many papers make leaps from one sentence to the next that, if you're not familiar with the field, can take a couple days to figure out. Even then, real world proofs are informal and therefore not air-tight. They're close enough, almost always, but there's a reason why a mathematical proof isn't considered valid unless it's lived for two years under peer scrutiny.

One could drill down to formal proof in the Godelian sense, in which proofs are mere typography and can be checked mechanically, but that's not how most of real mathematics is done and, practically speaking, most of it can't be done that way and remain useful to humans (like assembly language, it's too low-level for most applications).

View on HN

> most of it can't be done that way and remain useful to humans (like assembly language, it's too low-level for most applications).

Sincere question (I'm not a mathematician): why can't it be done that way?!

On top of an assembly language you can create a higher level language and on top of that an even higher level one, and it is airtight, it has to be or the code won't compile or will throw a runtime exception, the compiler or interpreter doesn't just "roll a dice" when it comes across and ambiguous statement! You just can't have ambiguous statements, so starting from a "precise" assembler everything else built on top can absolutely be "air tight" at the language level.

(Now concerning what the program actually ends up doing (like something else than you intended), or that sometimes you trade off security for speed and get a buffer overflow, ok, these things happen, but not at the language level! usually, and when they do - like C programs exploiting undefined but known for certain targets compiler behavior this is either advanced malicious obsfucation or random rookie mistakes.)

So explaining the question: why can't one build a higher level mathematical language bottom up, starting from an "assembler" of machine-checkable proof steps and building one or a few levels of higher level human-friendly languages that still map unambiguously to the lower level one?

Just because mathematical language has evolved in a top down fashion, starting with describing proofs in words or symbols derived from words, and then developing more an more precise language and systems, it doesn't mean that one can't go the reverse route, bottom up, an maybe meet closer to the top in a way, so that the resulting new mathematical language will be similar enough to classical one not to scare everyone away, right?

...and the benefits seem immense! Imagine:

(1) replacing years of peer review replaced by machine checking basic correcting (+ some machine testing on huge data samples, for testable proofs, just to be sure there was no bug)

(2) AI expert systems bringing real contributions to math by actually discovering new proofs AND providing them in a language understandable for humans, so humans learn from them and discover new techniques

EDIT+: (3) allowing the development of much more advanced theories, because just as in software you can build much larger systems once you learn how to write more "bug free" code, the actual complexity of the proof could be much larger and maybe new realms of mathematical will become accessible to human understanding once we have a "linguistic aid" to reducing the percent of faulty proofs and the time spent debugging them

This is a very good thought. Some current projects are trying to develop computable mathematical foundations in a more structured way. Homotopy type theory (http://homotopytypetheory.org/) is one example that has a lot of buzz around it just now, but automated theorem proving has been trying to work with higher-order concepts for ages now.

In the classical approach of "compiling" everything into sets/logic/etc., you end up with just the assembly language problem that's being discussed, where all the high-level structure vanishes. In order to do your bottom-up approach instead, one of the things that needs to happen is to make the theory really compositional, so that once you've defined some abstraction or higher-level concept, you can use it in constructions and proofs without having to break the abstraction. You don't need to know - and in fact you shouldn't be able to find out - just how the natural numbers were constructed, as long as they work by the right rules. This motivates the use of type theory to describe mathematical objects, and say which operations are allowed. We want to be able to add two numbers and get another number, but we don't want to be able to intersect two numbers as if they were sets, even if they happen to have been built out of sets.

So I think you are right - or at least, there are plenty of people who agree with you that this is a good idea. It is difficult to actually do, of course, but that's life.

> We want to be able to add two numbers and get another number, but we don't want to be able to intersect two numbers as if they were sets, even if they happen to have been built out of sets.

Can't we do this in current mathematics?! I mean, no physicist or engineer ever thinks of numbers as sets, even if you are the kind of physicist that reads and understands mathematical proofs.

The vast majority of working mathematicians work in set-theoretic foundations, in which numbers are sets.

Right, this is how mathematics really works. But formalizations of mathematics may suffer from leaky abstractions. If we prove facts about numbers by compiling them into sets, and then using set-theoretic axioms, we might accidentally make it possible to prove things about numbers that are incorrect or meaningless.

Isn't this an abstraction problem that you solve by simply providing an "interface" or equivalent concept or access specifiers in oop like private/protected? All other modules that use the number module for applied math will just see an "interface" (let's call it GeneralNumber - as far as I know there are a few other alternate ways of defining numbers besides sets, right?), and the particular "implementation of numbers as sets".

For more abstract algebras or who knows what, the "numbers module" might also implement another more advanced interface that exposes more of the implementation, a "SetsNumber" interface. If you know have a proof that uses this interpretation of number that is tied to one particular "implementation", then there is nothing incorrect about it leading to weird or "meaningless" results, they would be correct for SetsNumber but not for GeneralNumber (or someone might need to take a good look and see if they can be made to work for GeneralNumber too).

(I know, the words are all wrong, it probably sounds either "all wrong" or like a gibberish to mathematicians that don't also happen to be programmers ...someone should figure out more appropriate terms :) )

And about leaky abstractions, I think they happen a lot in software because of the tradeoffs we make, like 'but we also need access to those low level stuff to tweak performance', 'but we need it done yesterday so it's no time to think it through and find the right mode' or 'our model has contradictions and inconsistencies but it's good enough at delivering usable tools to the end-user, so we'll leave "wrong" because we want to focus on something that brings more business value right now' etc. Also, there's a biggie: for some problems using no abstraction is not good enough (initial developing/prototyping speed is just to small), but if you figure out the right abstraction it will end up being understandable only by people with 'iq over n' or 'advanced knowledge of hairy theoretical topic x', and you can't hire just these kinds of people to maintain the product, so you knowingly choose something that's leaky but works and can be maintained by mediocre programmers, hopefully even outsourced :)

Yes, the interface idea is basically the right thing, but there are technical difficulties which aren't immediately obvious. For example, we'd like to be able to prove that two different implementations of the natural numbers are equivalent (one can do this mathematically, so if our system is going to handle general mathematics then it has to be capable of doing this). So we have to think quite hard about what this "equivalence" actually means. It's not enough to say that they satisfy the same axioms, because in general there can be all kinds of models for some set of axioms. It's closer to say that all number-theoretic statements about numbers-v1 are true of numbers-v2, and vice versa: but you can see that this is starting to get a bit hairy in terms of computable proofs.

A related problem, which speaks to the leaky abstraction issue, is "proof irrelevance". Typically, if I've proved something, it shouldn't matter exactly how I did it. But it turns out to be tricky to make sure that the proof objects in the system don't accidentally carry too much information about where they came from. Sure, you can define a way to erase the details, but you still have to prove that erasing doesn't mess up the deductive system.

None of this is insurmountable, but it's a glimpse into the reasons why encoding mathematics computationally is not trivial.

Because until very, very recently, we simply haven't had the means to compute any proofs that mattered.

Rendering even relatively simple high level concepts in to low-level structures and then deriving them in the basic steps takes massive amounts of resources. At least one proof took over 15,000 pages of text (had you printed it).

A secondary problem (which we've been working on for a couple decades now) is that we lack the machinery to translate the results back in to something human readable. At some level, mathematics is about the ability of humans to understand the relationships between things, so computer proofs that only the computer understands don't really help us - especially if we can't relate them meaningfully to our other knowledge.

I mean, people have been trying for hundreds or thousands of years - it's just kind of a hard problem.

We do have automated theorem checkers that follow your idea: from a very simple set of axioms you can build higher level lemmas and proofs that are all mechanically verified by a small trusted logical code. Its actually a very rich and fruitful research area that also happens to live quite close to computer science! Many of these proof checkers are actually just programming languages with a very fancy type system.

However, I don't think we will ever see math move to a totally computer-verified schema like you mentioned:

* First of all, its very hard to write the rigorous proofs that can satisfy a computer. Do you know that feeling when you know that your program will run just fine but the type checker is being picky about a technicality and wont accept it, meaning you need to refactor lots of stuff to appease it? Mechanically verified proofs are like that but the typechecker is even pickier!

* Often, there is a big disconnect between the important mathematical ideas and the logical foundations they build upon. For example, differential calculus has a very simple intuition (rates of change, areas under curves, etc) and can quickly biuld into applications, but its actually pretty hard to build it from basic principles. In fact, it took hundreds of years until mathematicians finally figure that part out and in the end the foundations were totally different from what they were when they started. If you tried to model this in a computer, the effect would be having to rewrite all the foundational proofs and breaks tons of interfaces and higher level lemmas as people started to learn about all the corner cases in the system.

This post ignores the central driving force behind why mathematicians do mathematics: mathematics was created by humans for their own pleasure. It's a coincidence that they find such useful applications in the real world, and mathematicians mostly don't care (it's like a bonus if someone finds a nice application of your work, and maybe it provides you more grant money).

In this light, why would any mathematician want to replace peer review with machine checking? It would result in two undesirable things: 1) you'd have to submit papers in a machine-checkable format, which very few people enjoy writing because it's not a natural language to do high-level reasoning in. 2) you'd lose the chance for others to tell you whether they think your research is interesting or not, relate it to other work, give their own conjectures or ask about clarification, which is the real reason for the peer review system. Overly complex proofs with subtle mistakes are few and far in between.

Similarly, why would we want to offload the joy of finding proofs and discovering new techniques to computers? That's like proposing we have computers produce all art and music. The process of creation and discovery is largely what makes mathematics worth doing!

I understand what you say. But my interest is actually into AI, so the same way you find pleasure in creating and understanding interesting proofs, I find pleasure in trying to think about how the human mind works and how to make artificial forms of intelligence that share the properties of human mind but not the damn limitations of the "biological hardware" and of mortality. And I also think that in fields like AI "proof by engineering" is the only way to move forward - we'll have to build them or 'evolve them' in order to prove that they can be built (I know, this is not a line of thinking that mathematicians enjoy :) )

I'd love to see AI evolving to the level at which they create art and music or analogues of these (for their own pleasure and maybe for that of humans too, if the pleasures are compatible).

I know, you'd have to share my belief that strong AI is possible (and really close too I think) and that that minds are nothing but machines themselves and that all forms of intelligence will be comparable, regardless of whether the hardware will be "biology" or "technology", "natural" or "artificial" (in a few hundreds years I think we'll even cease to make the difference between these concepts, they will appear synonyms to our non-human or not-so-human-anymore descendents, just some linguists will identify different etymologies of them) :)

This is the right attitude; more power to you!

Just don't try to justify it by its "benefits" for mathematicians.

Apparently there have been some interesting advances in this area recently:

http://cacm.acm.org/magazines/2014/2/171675-a-new-type-of-ma...

I think it can in theory, but the reason it hasn't been done in practice is basically that mathematics is too damn big. Look at Whitehead and Russell's original attempt to do basically exactly what you're asking for: it took them a few hundred pages to build up enough machinery to prove that 1+1=2.

I never got to why this kind of work was stopped.

I only heard the same argument (this is the phrasing from Wikipedia but everybody seems to say something along these lines):

>"However, in 1931, Gödel's incompleteness theorem proved definitively that PM, and in fact any other attempt, could never achieve this lofty goal; that is, for any set of axioms and inference rules proposed to encapsulate mathematics, there would in fact be some truths of mathematics which could not be deduced from them."

...so what?! The fact that there can be truths that can't be deduced from an "assembler language" just means that the system will sometimes just say something like "error: no proof in the current model database for 'fact x' found" and then the mathematician will just add "consider 'fact x' proven as in the defined in modelXYZ" (a model that can have a totally different logic than the current one - think of a model as a library written in a completely different programming language, in software analogy), taking responsibility for the fact the equivalence of the concepts 'fact x in current model' and 'fact x in modelXYZ'.

The long term goal would be unification of as many of the models as possible (even with, what I understand from Godel, as the impossibility of total unification - if something is proved to be impossible, it doesn't mean you can't get great benefits by always getting asimptotically closer to it) preventing such "forced equivalences", but it would still be a working system in the meantime. And more importantly, I guess, the system will make the "forced equivalences" obvious, and label them as problems for mathematicians to solve.

It wasn't stopped, it's just way, way harder than one would naively expect. Russell continued to work on it by developing type theory, which was later carried on by people like Alonzo Church and Per Martin-Löf. This led not just to types in programming, but also to the use of types in proof checkers like Coq and Agda, which are very much the kind of thing you're talking about. Efforts are ongoing to continue working towards the vision of automated theorem proving, but again, it is an extremely difficult problem.

Part of the problem is, how do you know you can't prove it rather than just that you haven't proved it, without some kinda of metatheory framework?

Reply on news.ycombinator.com