Hacker News Reader

Comment by danharaj | Hacker News Reader

> Mathematics is very strict science with axioms and following theorems.

Mathematics textbooks would be intractably longer if they spelled out every step in explicit, formal detail. And then the proofs wouldn't make sense to people because the core ideas would be obscured by the formality! A typical mathematics proof is intended to be read by a thinking human assumed to have some level of mathematical sophistication and knowledge. These assumptions make proofs far more implicit than proofs in a formal language, which essentially only assumes that the "reader", i.e. the computer, can push symbols around and compare them.

View on HN

This is a common objection from mathematicians, that is very understandable. I think both Lamport and Voevodsky’s have made important contributions here [1]. Namely in presenting idea from software that we use to manage _exactly_ your complaint.

The way in which mathematicians structure proofs has fallen behind the ways in which software engineers structure programs (which are isomorphic to proofs). The question is then to develop languages which encompass these modern methods.

This is really the goal of the homotopy type theory project, to provide a language which is both machine checkable and easy to use informal reasoning with.

[1]https://www.microsoft.com/en-us/research/publication/write-2...

https://www.youtube.com/watch?v=kOY-XE29_d8

It's also important to note that this situation is _precisely_ what Voevodsky wanted to prevent:

For nearly a decade, Voevodsky has been advocating the virtues of computer proof assistants and developing univalent foundations in order to bring the languages of mathematics and computer programming closer together. As he sees it, the move to computer formalization is necessary because some branches of mathematics have become too abstract to be reliably checked by people.

“The world of mathematics is becoming very large, the complexity of mathematics is becoming very high, and there is a danger of an accumulation of mistakes,” Voevodsky said. Proofs rely on other proofs; if one contains a flaw, all others that rely on it will share the error. [1]

Most mathematicians still think of machine check for dealing with a large _number_ of cases; but Homotopy Type Theories goal is to manage abstract complexity not just size.

[1]https://www.quantamagazine.org/univalent-foundations-redefin...

I own a copy of the HoTT book :)

> Namely the way in which mathematicians structure proofs has fallen behind the ways in which software engineers structure programs (which are isomorphic to proofs).

The problem is that the required structure for writing sophisticated mathematical proofs is much more demanding than even a piece of software as complex as the Linux kernel. Part of that is because software as such, when interpreted as proofs, don't verify properties nearly as strong as a real theorem. The difference between a proof of `Integer -> Integer` and `Integer -> Odd Integer` is already a gulf the vast majority of software does not bridge.

We're just not there yet. Voevodsky's program is a great first step but just that: A first step. No one really knows what the next thousand steps will be. It's not straightforward at all.

I agree completely that the tooling is not there today.

However:

"The problem is that the required structure for writing sophisticated mathematical proofs is much more demanding than even a piece of software as complex as the Linux kernel. "

Mis-understands why and how we use the linux kernel. Linux isn't that difficult to understand really (both in LOC, and the abstractions it presents). It's simply a base which can be relied on that provides abstraction points we can interface with (both as software, _and_ hardware_).

The important part here is that not only does linux give us a reliable "library" of behavior, but it is one that is common and reuseable.

This "library" of behavior is something we've begun to see present itself in category theory. This is why so many modern papers start with "we show that there exists a isomorphism...".

The biggest thing _modern_ computing and libraries focuses on is composition of behavior. Aka functions that take functions. If a computational interpenetration of uni-valence is found we will have similar capabilities in math (e.g. making it possible to simplify the process of moving between isomorphic structures). I believe this would be a major stride towards broader use of machine verification.

Speaking of Lamport's "How to write a 21st-century proof" paper, here's a video of a great presentation he gave on this topic last year:

https://www.heidelberg-laureate-forum.org/blog/video/lecture...

> The way in which mathematicians structure proofs has fallen behind the ways in which software engineers structure programs (which are isomorphic to proofs).

If we accept that a software program is isomorphic to a proof, is there anything that isn't isomorphic with a proof?

I can prove Pythogoras' theorem with a diagram, so by extension anything in the physical world is a manifestation of mathematical theory and, since it exists, is isomorphic with a trivial proof for something.

>I can prove Pythogoras' theorem with a diagram

I don't think I agree with this statement. As a matter of fact, I've always had a deep unease with so-called "geometric proofs", where a succession of visual transformations of a diagram are used to prove a theorem.

You can certain explain the intuition behind the proof of Pythagoras theorem with a diagram, and there's huge pedagogic value in doing that.

But to me it isn't a formal proof until it has been codified in a language that a computer can walk from start to end making sure each step is valid.

scratches head I'm pretty sure I can come up with a codified language proof that you will accept, then define a mapping between the language and transformations of a diagram. And while not an expert on isomorphism, but I'm pretty sure that makes the visual proof isomorphic with the codified language and hence valid (and, indeed, computable).

Basically, although code and proofs are in a sense isomorphic, I think everything and proofs are isomorpic in the same sense. So claiming that proofs should be structured to the same standards as code because code is isomorphic to proof is a bit of a non-sequitur. Why not show the layout of my rock garden is isomorphic to code and hence proving something (my rock garden can be Turing complete) and then claim my rock garden should be structured like a program?

Basically, the idea that the structure mathematicians favour for proofs have fallen behind programmers laying out of code is not well substantiated and the idea that 'proofs are isomorphic to code' is not useful because it is far too broad.

It's not so much that programs are isomorphic to proofs; it's that mathematics and programming are the same activity. It's essentially a historical accident that the people who practice this activity have ended up in different groups, and that those groups use different terminology for the same things ("program" vs "proof", "type" vs "proposition", "execute" vs "simplify", "tuple" vs "conjunction", "union" vs "disjunction", "function" vs "implication", "dependent function" vs "universal quantification", "interface" vs "existential", "programming language" vs "logical system", etc.).

All of the relationships between these are the same too (e.g. a program `p` has type `T`, iff the proof `p` proves the proposition `T`; the proof `w` proves that the existence of `x` implies the proposition `y AND z` iff the program `w` is a function which generates a tuple of `(y, z)` when given an argument implementing the interface `x`; and so on).

Mathematicians and programmers do care about different things. Mathematicians are more concerned with informally proving previously unknown results; which corresponds to something like learning that a type has a value by sketching some pseudocode. Programmers care deeply about how many steps their proofs (programs) take to simplify; how easy it is to modify a proof to prove a slightly different proposition, etc. Yet there are so many good ideas on each side that are immediately applicable (e.g. dependently typed languages take rigorous logical systems and view them as programming languages; proof engineering takes software engineering ideas and applies them to building and maintaining proofs).

I'm struggling to think of an activity involving rock gardens that corresponds precisely to, say, universal quantification.

Note that there are formal, machine-checkable languages to describe geometric proofs: http://lambda-the-ultimate.org/node/3899

Of course, that still leaves the same problem of explicit proofs being tedious, i.e. being able to prove pythagoras's theorem "with a diagram" does not mean being able to prove it "within an explicit, formalised diagram language".

I'm inclined to agree with you; though the key word here is "trivial".

Types are propositions, and programs are proofs of their types. Unfortunately most programs are overly-complicated proofs of trivial propositions (when looked at from the mathematical side of curry-howard; of course what's actually the case is that we tend to only use types to specify a tiny part of what our programs are meant to do).

In an untyped language every expression has the same type (which we might call `Thing`, and contains integers, strings, functions, etc.) so in the curry-howard sense every expression is proof of the same trivial proposition.

I'm inclined to think of the laws of physics (whatever they are) as a programming language, and physical systems as programs running in that language. On first impression, it doesn't seem like physics is typed; hence every physical system is a proof of a trivial proposition (essentially: physical things can exist). It would be interesting to hear a counterargument though.

Note that in these cases it's the types/propositions which are trivial, not necessarily the programs/proofs. Consider that we could, if we wanted, prove a pretty trivial proposition like `((A -> B) AND A) -> B` in a roundabout way that involved applications of Fermat's last theorem. I tend to call such things "(over)complicated", rather than "complext", since their complexity isn't inherent or required.

Why can't textbooks use code-folding style display to hide unwanted detail? Paper books are basically obsolete except as a master copy for archival.

I participated in a discussion on /r/math about this a few months ago, and there was surprising resistance to ideas like this. Most of it fell into two categories. The first was people with a paper fetish who refuse to believe that there are now computer display technologies that provide adequate readability and resolution to be a full-time substitute for books. The second was people who can't imagine a usable way to typeset proofs that embed metadata about which lines are the key steps and which could be folded. This is probably influenced by the fact that LaTeX doesn't support this kind of semantic markup and it would be awkward to add.

people with a paper fetish who refuse to believe

Maybe there was surprising resistance because you spoke like that?

Nah. I'm only using language that harsh now because of how disappointingly irrational and weak the objections on reddit were. It's odd to see mathematicians resistant to quantifying what they believe to be inferior about computer displays, and improperly generalizing what seemed to be their experience with $500 laptops to also argue against high-quality eInk, OLED and IPS LCDs.

It's odd to see mathematicians resistant to quantifying what they believe to be inferior about computer displays

They're mathematicians, not display interface experts. This is like demanding that someone explain to you why they don't like a particular kind of food -- people are allowed to dislike things without having a complete internal axiomatic system justifying it.

Dislike, sure. Personal preferences are acceptable. But claiming that it's impossible for a computer/tablet display to be as readable as paper and that all electronic displays cause more eyestrain is unreasonable. Especially when the person making that claim has already demonstrated that they are familiar with terms like resolution, contrast ratio and form factor, but they fail to even propose a hypothesis for what might still be inferior about the best computer display technologies.

Mathematicians are happy to use computers for typesetting papers, but not for the initial creative phase:

1) computer displays require you to scroll, which interrupts your mental flow

2) paper and pencil or pen is free-form

3) in advanced mathematics, results are rarely calculated in numerical form, so the computer isn't helpful

4) notebooks are permanent. No backups needed.

I imagine the same is true for most cartoon artists.

Two points:

1) Mathematicians write all over the papers and books they read. Electronic versions of this exist (e.g., Xournal, written by a well known mathematician), but they tend not to be as convenient as simply scribbling on paper.

2) Mathematicians digest papers nonlinearly. Digital presentations don't usually lend themselves to flipping back and forth between pages. At times, I suspect mathematicians use papers and books as memory mansions, organizing concepts by relating them to their location in the physical copy.

> Mathematicians digest papers nonlinearly.

That's a fairly weak argument: you can browse an electronic document in a non-linear fashion way easier than a book.

And also: books don't have CTRL-F

> That's a fairly weak argument: you can browse an electronic document in a non-linear fashion way easier than a book.

How do I make handwritten side notes? How can I create a bookmark for a specific page? How can I view multiple non-contiguous pages next to each other? How can I reference a specific part in an electronic text (in non-electronic text "3rd paragraph on page 11") and send it to a collaborator?

I was specifically addressing the "non-linear" part, and none of the things you list have anything to do with that.

However, to nevertheless address your points:

>How do I make handwritten side notes

There is a number of applications to do this (e.g. xournal), and when combined with a touchscreen on a decent hirez modern device, we're getting close to what paper can do. I'll grant you: this is still the weak point of computers as compared to pen and paper (especially for scribbling diagrams), but it won't be for long.

>How can I create a bookmark for a specific page

I'm not sure if you're trolling here, all e-book readers I've used have this feature.

>How can I view multiple non-contiguous pages next to each other?

Multiple windows ? CTRL+N ?

>How can I reference a specific part in an electronic text (in non-electronic text "3rd paragraph on page 11") and send it to a collaborator?

Cut and paste?

Or ... sending him an email with ""3rd paragraph on page 11"" in the body?

I think if you reframe the problem it can be much easier (if not trivial) to find solutions.

If you present a 100 page book as a folder of 100 image files instead, most of these become image manipulation problems:

>How do I make handwritten side notes?

The same way you'd edit an image.

> How can I create a bookmark for a specific page?

Create a subdirectory with the page or a link to the page.

> How can I reference a specific part in an electronic text (in non-electronic text "3rd paragraph on page 11")

Cut and paste the excerpt into a new image file.

> and send it to a collaborator?

File sharing is a solved problem. Hell, you can even share it on Instagram if you so choose.

a lot of mathematicians prefer chalkboards over whiteboards too, because 85% of all known whiteboard markers are nearly empty.

love of math and love of technology aren't as closely linked as you believe.

> improperly generalizing what seemed to be their experience with $500 laptops to also argue against high-quality eInk, OLED and IPS LCDs.

And what Grad student can afford those at [Insert State University]. I was a PhD student in math not long ago, and vastly preferred paper books, and even printed out articles. It is way way easier on your eyes than something actively blasting light. Maybe in 20 years high quality e-ink will be cheap enough, but that has been promised since forever.

> It is way way easier on your eyes than something actively blasting light.

See, this is the kind of bad argument that really irks me. There are good arguments about how computers aren't ready to replace pen and paper for actively doing math, and even a few shortcomings for computers replacing paper textbooks. But "actively blasting light" doesn't mean anything. Photons are photons. If you think a backlit display is somehow harder on your eyes than an indirectly-lit piece of paper, then you should be trying to figure out whether you simply have the backlight set too bright for your surroundings, or if your screen's contrast ratio at reasonable brightness levels is inadequate. Your LCD's default settings are probably optimized for movie-watching more than reading, but that's easily fixed and definitely not an inherent limitation of all backlit displays everywhere.

>not an inherent limitation of all backlit displays everywhere.

This may be true, but in my experience(not very wealthy, typically sub $400 devices) the presets are set such that 0% backlight in the OS is glaringly bright. I cannot turn it down without rooting the device.

Maybe for tech device things we should have two separate tracks, one for wealthy snd people who can modify devices and one for poor and people who cannot. Even my Thnkpad laptop under Ubuntu has a setting for 10% brightness which is far too high for a truly dark room. The next lowest setting is 0% which is absolute dark. How do you use your laptop under such conditions?

I don't see how backlight settings for a truly dark room are relevant here. I've been annoyed by several of my devices being unable to dim far enough, but never in a situation where I would expect to be able to easily read words printed on paper. An office or classroom setting that has adequate light for pen and paper work could be too dim for an LCD at 100% brightness to be comfortable, but almost any device can be dimmed enough for that environment.

Color temperature can also be a problem, but there's a lot of awareness of that issue nowadays. Most operating systems now support automatic adjustment of color temperature based on time of day, plus manual adjustment. Devices that adjust their color temperature to account for ambient lighting are starting to catch on, and I expect they'll be pretty common in a few years.

You could use xbacklight to have a finer control of the display brightness. You can also rebind the brightness keys to shell scripts that use "xbacklight -inc <percent>" or -dec, with a finer resolution.

Trying to do learn math with a computer is frustration. The computer eats up your desk space, you have to constantly move it around as you work on different things, a mouse and keyboard eat up even more space. You have to have power, and you have to drop your pen every other time you need something.

Maybe you don't see the problem because you aren't doing any math?

I’ve been studying undergrad maths for the last year or two, and I had a bit of a breakthrough when I realized how much more effective it was for me to do all my work (notes, exercises) in LaTeX rather than with pen and paper. I can refactor at will, improving proofs, and the consistent tidy typesetting makes me think more systematically about the problem I’m working on.

I've started doing everything in LaTeX - diary, everything I'm learning about, books I'm writing, maths, documenting my programming etc - the last few months too; it's going great. It took a few months to learn about LaTeX packages, basic TeX etc. (And every time I use TikZ I've forgotten it all again..) It's especially useful mathematically in avoiding errors when doing page-long calculations with pen and paper - copying lines instead of writing them out, and the whole thing looking so lovely and neat - eliminates 95% of the errors I made before, and it's faster. I still do ideas, sketches etc on paper, but anything that's likely to be want to be kept goes straight into LaTeX.

But also..all my favourite books have markings on each page, margin comments, turned-over corners etc. Any pdf book I read more than once or twice, I'll get a paper copy, I think.

What tool(s) do you use for working with LaTeX?

A Makefile to encapsulate all the details of how to generate the PDFs.

Text editor customizations to trigger `make <current-doc>.pdf` on save. (Emacs in my case)

A PDF viewer that reloads the PDF when it changes on disk (Skim in my case, which does auto-reload, but I also have some Applescript in the Makefile to poke Skim so that it notices the file change faster).

A good text editor LaTeX editing mode (Emacs in my case).

Random test editor customizations for working on LaTeX.

My main tips are

1. don't be shy of perfecting your work environment

2. use git to track both your work environment customizations and your LaTeX work.

Except... it's not a fetish. Paper books have many advantages. It is easily annotable. (none of the current ebook types are easy). It provides tactile feedback, which can be used for organization - folded corners give you two types of indices (top/bottom outer corner). The entire structure of the book as a stack of pages gives you immediate visual feedback where you are, and it's effectively random-addressable. ("Yeah, it's roughly a third in, check there"). Heck, you can color page edges to make it even easier, and that gives you three spatial indices on top of the two tactile ones. It's not as unwieldy as screens. It is flexible, which makes it nicer to handle. It doesn't need to be charged. It doesn't break when you drop it. (Not to mention you can kill a fly with a paper book, ebooks don't work)

Yes, e-books have other advantages - but calling it a paper fetish basically means you're making an uninformed call, because you're not even aware of the advantages.

The second, you could have easily addressed by proposing a markup if it were easy to do so. The fact that you haven't, and aren't even aware why people think it's hard, means you're again coming from an uninformed position.

And you thought the resistance was surprising?

Paper math books also do not serve up distracting ads.

Math ebooks shouldn't either lol

The reddit thread in question was surprisingly lacking in discussion of the usability aspects you're focusing on. I think most of those issues make for a much more productive conversation, because there's real room for improvement in those areas—paper and current computer/tablet technology each have their own usability pros and cons. I'm not at all uninformed about those usability challenges. I was just surprised and disappointed at how many people assumed that paper had an unbeatable advantage on the purely visual aspects of presenting information, as if computers were still limited to 100dpi with really poor black levels.

> The second, you could have easily addressed by proposing a markup if it were easy to do so. The fact that you haven't, and aren't even aware why people think it's hard, means you're again coming from an uninformed position.

I didn't propose any specific markup because the specific syntax isn't the problem. The problem is that the predominant markup language for mathematical documents is LaTeX, which is a bit too presentation-oriented rather than semantic/structure-oriented for it to be really easy to use it to produce documents that can be interactively folded (especially when the output file format is almost always PDF). Something that used eg. MathML and an HTML/XML based overall document structure can trivially encode all the information necessary for rich interactive reading, and proposing specific tag or class names to indicate what lines of a proof should be collapsed by default only invites bikeshedding.

I think you're quite unjustified in accusing me of being so thoroughly uninformed.

Actually latex would be quite sufficient, basically what you are proposing is an appendix where you list additional details

The real reason people don't do this is simple, it would require an inhumane amount of work and details which will likely be wrong themselves and will for sure be to boring to be checked. Most science is wrong in some aspects, sometime it is better to have a meaningful intuition that can be understood by other expert (and maybe rejected)

>I was just surprised and disappointed at how many people assumed that paper had an unbeatable advantage on the purely visual aspects of presenting information, as if computers were still limited to 100dpi with really poor black levels.

I'm not surprised. Virtually all "designers" think low contrast text is better, despite high contrast being preferred on paper. They deliberately reduce contrast by setting the text color to gray. Even Firefox's Reader View, which otherwise fixes most mistakes of designers, sets the text to gray unless you override it in userContent.css. Desktop GUIs often have low contrast text too, which is also difficult to fix. Unless somebody somebody knows how to do this their expensive monitor will be wasted.

Why can they? You can't assume fully explicit proofs are practical just because they're plausible. The justification of practicality will be highly nontrivial. If its impractical to write such a textbook then code folding gets you nothing.

If it is impractical now, that simply means the software needs improvement. If mathematicians stop being so accepting of informal proofs then there is a very strong incentive to improve the software.

> that simply means

The point is that it's not simple. It will require significant advances in computer science.

In all of my papers, I have attempted to include an indent-based hierarchy of the argument. Adding code-folding to this would allow for so much more detail here.

I don't think we should have papers being nothing but folds, but there is definite value in presenting proofs in this way.

One potential downside is that there is no longer an order that guides the reader through the paper. Because it isn't quite clear how deep the author expected you to unfold an argument.

Maybe a default path through the document could be specified by the author or by convention

I think the idea is that you go deeper only if you are stuck or unsure about something at your current level.

Is code-folding necessary? Instead you could put the demonstration in an appendix, and the authors would be free to decide what goes in the core of the article and what goes into the appendix. This could be made automatically where trunks of article would move back and forth from the core to the article and vice-versa, depending of what the reader chose to, and in each case a corresponding pdf could be generated.

You could say the same thing about code, yet we're able to build upon our abstractions to make something both high level and able to be broken down to the foundations.

Can't you make the formal proof software "smart" enough to prove a theorem given sufficient intermediate steps and hints about what other theorems/defs to use? i.e. basically what a book does? This would makes writing formal proof much easier, wouldn't it?

There is a big difference between explaining / teaching a proof and verifying its correctness. We're talking about the latter here.

> Mathematics textbooks would be intractably longer if they spelled out every step in explicit, formal detail.

Just as an example, Russell & Whitehead's Principia Mathematica famously requires some 400+ pages to prove that 1+1=2 (well, they prove some other stuff, too, I suppose.)

See the image and caption here to get a flavour: https://en.wikipedia.org/wiki/Principia_Mathematica

It's not so much to prove that 1+1=2; rather to set up the definitions and background entirely from scratch. If you had to define the grammar and vocabulary of English before you wrote a sonnet, your sonnets too would be exceedingly long.

Exactly right. Most of those background steps do things like establish the basics of complex numbers, and you can reuse them for anything else involving complex numbers.

The actual proof in metamath that two plus two is equal to 4 is at http://us.metamath.org/mpeuni/2p2e4.html

It is only 10 steps long. Yes, it is longer than an informal proof (such as one printed in a math journal), but it is not hard to follow. In this case this proof is rigorously verified by four different independent computer verifiers all the way back to the axioms of logic and set theory.

It is already possible to have proofs that are completely computer verified. Up to this point, mathematicians often do not use them because it is simpler not to. But in the long-term, I think we should change our expectations to start requiring proofs to be verified by computer if we really want to believe in them. Humans make mistakes, and reviewers often miss them. Computer verification, especially when there are multiple independent verifiers, provide much greater confidence that the claimed proof is actually correct. The number of so-called proofs that are actually not proofs is very large.

If you are curious about metamath, I have a video on YouTube that you might find interesting: https://m.youtube.com/watch?v=8WH4Rd4UKGE#

Someone already linked metamath, it also gives a flavor of just how long some proofs can be when you fully formalize them and start from ZFC axioms. From the trivia page at http://us.metamath.org/mpeuni/mmset.html#trivia "The complete proof of [(2+0i) + (2+0i) = (4+0i)] involves 2,863 subtheorems including the 189 above. These have a total of 27,426 steps—this is how many steps you would have to examine if you wanted to verify the proof by hand in complete detail all the way back to the axioms of ZFC set theory."

Depends on your starting point. You can prove 1+1=2 quite easily from the Peano axioms:

1+1=1+S(0) [definition of 1]

1+S(0)=S(1+0) [definition of addition, a+S(b)=S(a+b)]

1+1=S(1+0) [transitivity of equality]

S(1+0)=S(1) [definition of addition, a+0=a]

1+1=S(1) [transitivity of equality]

S(1)=2 [definition of 2]

1+1=2 [transitivity of equality]

It's like telling that there are thousands of machine instructions to be able to write printf("%.2f", x). It means that we should use the power of abstraction.

That was exactly the point, if you abstract then you are handwaving details (unless you abstract inside a formal system that itself defines methods for abstraction and then you are back to square one)

Reply on news.ycombinator.com