comments on "QED For Science"

[gusl]

Formalization may be my biggest intellectual cause.

I just asked someone to comment on my manifesto: A QED Project for Science: The Promises of Computer-Level Formalization. I just replied addressing his criticisms:

I guess my gut instinct is to say that half of the point of science is to figure out what logic such a proof should be written in. Scientific theories, by deffinition, are not complete.

I disagree with this. There are many phenomena that we understand
quite well today, and some theories are pretty stable, e.g. Newtonian
mechanics. Even though it is well-understood, this knowledge does not
have a formal representation in the computer, which means it's not
very usable if you're trying to do advanced information retrieval,
etc. However, to the extent that scientists understand the theory, it
*is* represented formally inside their heads...


> This means fundamentally that we don't know what logic they should be represented in yet. Maybe you could start on some core principles, but I feel like next week we'll just find out some new thing about quantum theory that breaks the entire model, and logic will have to be scrapped.

Well, the logic that I'm referring to is the logic we use for talking
and reasoning about things. We could use logics to model quantum
mechanics, but we will talk about this modeling (i.e. the scientific
argument itself) with this "common sense" logic. [it's not so clear what this should be]


> The fundamental difference here between math and science
> though is that math doesn't have to be concerned with facts.

Yes. This is why mathematical theories have fewer axioms. There are no
unknowns that the world gives us.


> Math can't
> suddenly change, it is merely a set of models to begin with, so using a slightly
> more formal model makes sense. With science our goal is to discover the
> model, constantly changing and morphing it, often scrapping it all
> together. In some sense scientists are always in the preliminary stages
> of working on a logic, and then disproving it. There are few sciences I
> think where we know enough to model it, and believe we won't scrap that
> model almost instantly. I.E. it's a lot of work to go through literally
> for the purpose of proving the model wrong (since that is in some sense the
> goal of science, to disprove it's own theories). In other words, it's
> not like we have most science's down to a science yet, by which I
> mean... a math.

You do have a point, that much science is done intuitively, without
much methodology. To the extent that a scientist isn't able to justify
a belief with rigorous logic, I would say that they don't understand it.

Anyway, my point is to try to extract theories from scientists' heads,
to the extent that the scientists already have them in their heads,
even if these theories are not very good and in the process of
evolving... and into the computer, where we can do cool stuff like
fast searching, checking for consistency, automated discovery, etc...
the computer could, for example, discover analogies that nobody has
thought of because the scientists who understand one subject area
don't understand the other.

Can you see how this connects to the idea of automatically generating
a math textbook, customized for the reader, etc?

To make an analogy, imagine that math is a 3D shape, but textbooks can
only show it in 2D... when a student wants to see the stuff from a
different angle, it should be possible for a computer to automatically
generate that perspective... but to do that, it will need a faithful
3D representation. Textbooks today are like 2D representations... if
you have a shelf-ful of textbooks presenting the very same subject,
this would give you several 2D images, from which you would hope to
reconstruct the 3D image (i.e. a faithful representation of math in
the computer).

But in practice, this probably won't work, or at least we would need a
shitload of data to learn from. It's much easier for textbook authors
to represent math faithfully in the first place (like using semantic
tagging on a web page, rather than just plain HTML), tagging things
with multiple representations, etc.