Technology for Which Mathematical Activities?/1

[Michael Lee Finney]

> The various postings expressing optimism about the use of technology
> based on current developments have NOTHING TO DO with what I am
> saying.

> For various specialized tasks of interest, there has obviously been
> more and more useful technology.

> For certain other tasks of even greater interest, progress appears
> totally unthinkable at the moment.

> I really was only making my obvious point IN PASSING. I was setting
> the stage for discussing what are the REALISTIC outcomes of proof
> technology research that have been OVERLOOKED and that I do think are
> FEASIBLE, although difficult.

> I will by the way defend attacks against me for finding TEX a
> disgusting nuisance. But I don't think that this is a useful
> discussion for FOM.

> Harvey Friedman

An example of how technology can help with mathematics is how I did my BA
thesis. This was a two semester course, where I was presented an open problem
in Knot Theory and had to find a solution. My approach was half mathematics
and half computer science. I built custom software to help explore the problem
space. That software was continuously modified as what I was looking at
changed. None of that was in the final thesis -- or in the follow up paper
with my advisor and a Masters student (an extension of my work and cleaned up
for publication, an area where I am still weak, especially when knowing what
to leave out).

This is not automatic theorem proving, but some of the edge cases may have
been very difficult to find without the use of technology, and discovery of
the final form of the solutions would probably have not been found. Going
forward, I see the use of custom software to assist with mathematics to be
more the rule than the exception. Many mathematical problems may benefit from
this type of approach to exploring the problem.

In addition, on the TeX side of things (although most people use LaTeX and not
TeX directly), I also released the logix package to CTAN with around 4,000
additional symbols, most of which are not found in Unicode. Some of the
overlap is due to symbol variants. That included a large number of symbols
allowing LaTeX to easily draw Knot diagrams. The font is designed to be
compatible with the AMS STIX Unicode fonts. I should note that LuaLaTeX or
XeLaTex (or the next version of LaTeX) is required since Unicode fonts are
used extensively. Its time to move on from Knuth's 8-bit font restrictions.

Being able to create new symbols on the fly is something that was originally
common, but has long been missing from mathematics. I'm sure we've all seen
books where the symbols have been hand written in the book after publication.
Technology is lifting those limitations. This is another area where technology
can benefit mathematics. We no longer have to use the same small set of
symbols when working with new mathematics. Sometimes, improving notation can
be as important as the work itself. Right now, LaTeX is the best way to do
that for mathematics. Programs like Equation Editor tend to be ok for simple
things, but fall short as one's needs increase.

Currently, I am building a Hilbert IDE -- which will be able to verify
Hilbert proofs in alternative logics. But, you are right, the format is very
precise allowing the verifier to "understand" the proof. There is an
associated BNF style grammar and parser based on the grammar. That could be
extended to remove the proof hints normally associated with a Hilbert proof. I
can see how to do that, but a bit of extra cost in time. A complete theorem
prover is much more difficult -- especially when classical logic cannot be
assumed by the verifier. Some of the major tools used by theorem provers are
no longer available. But, I can use specialized tools to help solve specific
problems.

Proof assistants for normal mathematical proofs are possible. Those might make
the input rigorous enough for routine theorem verification. The problem with
theorem verification is that proofs are written in natural language with many
things left out because they are understood by the indented audience. Every
such gap essentially requires a form of theorem proving. If a proof assistant
can narrow those gaps, then verifying complex proofs may well be possible.

I don't see space as much of a problem as time in this area, mainly due to the
explosion of the state space to be searched. Generally, the complete space is
never represented. And the different forms of AI technology that could be used
all have different constraints and different approaches. For example,
approaches such as neural nets may not be as effective as rule based systems.

Michael Lee Finney