Another semantic math wiki..

[Marty]

Hello all,

I was excited to see another project involving mathematics and the
semantic web.

With a small grant last summer, I designed a wiki (using Mediawiki and
Semantic Mediawiki, with other extensions), with the goal of
representing a large portion of "undergraduate mathematics", in a form
suitable for students and faculty. The semantics are used for project
management, as well as capturing the deductive structure of
mathematics. Semantic properties such as "relies on", "exemplifies",
and "specializes" are used, and querying and navigation can be
aided.

Although it is too early to widely publicize this project, I am eager
to meet potential collaborators, and I may apply for a larger grant in
the near future.

The goals of my "SlugMath Wiki" are different from vdash, SWiM, and
other projects which aim to encode mathematical knowledge on the
elemental scale. The SlugMath Wiki focuses on content created by
professional mathematicians, using familiar (to all mathematicians)
LaTex markup with a few minimal extensions to improve readability of
proofs. The semantics are used to enhance the content, by expressing
logical reliance and other connections between knowledge. My project
is not meant to automate theorem-proving or verification, nor to
represent the fine structure of mathematical sentences. However, my
project might be useful to guide more formal projects involving
automatic theorem-verification.

If you would like to take a look, I would certainly enjoy hearing
feedback. The following pages might be of interest:
* The main SlugMath wiki home page, at http://slugmath.ucsc.edu/mediawiki/index.php/Main_Page
* The "Basic Number Theory" cluster illustrates the automated
production of deductive graphs. http://slugmath.ucsc.edu/mediawiki/index.php/Clust/Basic_number_theory
* The definition of a group illustrates the automated listing of
examples. http://slugmath.ucsc.edu/mediawiki/index.php/Def/Group
* The help pages describe the project in more detail.
http://slugmath.ucsc.edu/mediawiki/index.php/Help:Contents

Please do not edit any pages yet, or further publicize the wiki.
There are further steps that should be taken before the wiki is
"released into the wild".

If you have any ideas about integrating projects, please let me know.
In addition, I am looking for PHP/Mediawiki programmers and
mathematicians to collaborate with, so please let me know if you are
interested. I can be contacted at weissman AT ucsc DOT edu.

best,

Martin Weissman
Asst. Professor of Mathematics
University of California, Santa Cruz

[nrolland]

Hello,

This wiki is a nice way to start a more intelligent math system, and
it is encouraging to see that pedagogical math on the web is gaining
traction.
Those properties like "exemplifies" express the different kind of
relationship concepts might have and will be able to generate
automatic navigational capacities. I can completely see how it can be
useful to navigate the graph of math notions to make sure one has a
thorough understanding of a field.



But, from my perspective, which might well be uncomplete, the core
added value of an intelligent (formalized ?) math wiki lies in the
variable substitution.
aka, if I discuss about the Klein set, and want to say it is a group,
the reader can, with the system's help, substitute the Klein's
specfics within the definition of a group. conversely, the more
advanced reader won't probably need go verify as it will be obvious to
him, having done mental substitution for groups a thousand time.
This property of variable substitution enables to deal with "code
reuse" so that each mathematician builds on top of another, just like
it's the case in real life, and that, equally importantly, the reader
experience is *decoupled* from the logical math construct, allowing
him to navigate at his level.

This is for me where the power of computerized math really lies (and
that I really hope to see in my lifetime..)

regards,
Nicolas Rolland

> *  The main SlugMath wiki home page, athttp://slugmath.ucsc.edu/mediawiki/index.php/Main_Page

> *  The "Basic Number Theory" cluster illustrates the automated
> production of deductive graphs.  http://slugmath.ucsc.edu/mediawiki/index.php/Clust/Basic_number_theory
> *  The definition of a group illustrates the automated listing of
> examples.  http://slugmath.ucsc.edu/mediawiki/index.php/Def/Group

> *  The help pages describe the project in more detail.http://slugmath.ucsc.edu/mediawiki/index.php/Help:Contents

[Marty]

Hello Nicolas,

Thank you for the reply and feedback.

I agree that a formalized math wiki offers significant added value,
but I think that formalization adds little pedagogical value. As a
math professor, I do not see my students struggling with mental
substitution, as I think you are describing. I think that most
linguists would agree that substitution is an innate mental process --
every person who uses a natural human language constantly
substitutes. I find that students have a bigger problem with
"oversubstitution" -- I will give two examples:
* Small children automatically put an "s" on the end of every word,
in order to pluralize it. They effectively substitute any noun for
any other noun. They have to be specifically told about exceptional
words.
* School age students tend to incorrectly apply the distributive law
to square roots, following the false rule "the square root of a + b
equals the square root of a plus the square root of b". They mentally
substitute any operation for multiplication, and have to be
specifically corrected.

So in general, I would argue that students would "over-reuse".

On the other hand, the problem that you mention is a significant one
for computation and automatic theorem-proving/verification. For
automatic proving/verification, it seems that this vdash project is an
excellent idea. For computation, I could imagine adding a tab for
"SAGE code" (SAGE is a great piece of open-source math software),
which describes how to construct a given mathematical object within
SAGE. SAGE can handle a great amount of abstract math, and can
perform the sort of "substitution" you are discussing.

I would also say that when mathematicians "build on top of another",
they do so by applying previously proven results and definitions to
prove new results. As a mathematician, I build upon other published
results constantly -- the process is not at all formalized like "code
re-use", though that is a reasonable metaphor. Perhaps the argument
for formalization is the (perceived or real) unreliability of the
mathematician's deductive method. It is essentially impossible for
nonmathematicians and computers to verify the results of math papers,
since the deductive reliance is almost never completely and clearly
stated. It is difficult for mathematicians to verify the results of
math papers too -- this is why I usually take months to referee a math
paper for a journal.

Personally, I think that the formalization of research mathematics in
my field (automorphic forms and representations) would be impossible -
but I think that the formalization of certain foundational fields
could be important and useful.

best,

Marty Weissman

[Caro Williams]

Hello, Marty, Nicolas, and others!

I've been following the discussion, as I'm greatly interested in the wiki development, and although my focus is more on math education than math, I thought I would jump into this conversation briefly. 

Marty, it seems that overuse in the way that you exemplify it is actually a symptom of the substitution difficulties that Nicolas notes, and having such tools built into the site would be useful.  Students--or any people unfamiliar with certain rules, exceptions, or concepts--will mis-apply or "oversubstitute" when they aren't fully familiar with the strategies they're attempting to apply.  Obviously, this raises multiple pedagogical issues, most relevant of which here is:  how do we provide the tools to become familiar?  Nicolas' substitution idea provides in-depth and thorough information consistently at the point of need in a way that's not overwhelming but is personally customizable.  (Not to mention the great number of students that bemoan how much math they've forgotten--"But I used to know that!"  This sets up a brief way of reminding that may stimulate recall of rusty skills...) 

I'd also like to add a purely personal note, that as someone who is only peripherally involved in the mathematics community, I don't use formal math terms as often in my daily life as I used to.  Sadly, this means that I often forget the labels of concepts--once a quick reminder is given, then I remember and can apply my conceptual knowledge.  Today at brunch a colleague was talking about the "comparative advantage" economics model, and while the phrase "comparative advantage" evokes some relevant meaning, it wasn't until he mentioned Portugal and England trading wine that I began to remember a brief encounter with that topic some years ago.  My point is, that the word "groups"--in Nicolas' example--won't be enough for everyone that's interested in learning about Klein set.  They may remember enough to keep going, but they may also have forgotten some key parts of the concept that relate meaningfully to the Klein set.

It seems here that the conversation is blending pedagogical goals with formal mathematical advancement very nicely--it can be a difficult balance.

Take care,

Caro Williams

[Marty]

Maybe I'm a bit confused about this Klein set/group example that
Nicolas indicated.

I've taught group theory on many occasions to undergraduates and
graduate students. I have never encountered a situation where I or
students have "discuss[ed] about the Klein set, and want to say it is
a group". I don't really know what is meant by this, perhaps.

Maybe you mean that a composition table is given on a set with four
elements, 1,i,j,k, and you are telling students that the composition
table satisfies the group axioms.

On my wiki, I have given the composition table on this set, and then a
semantic link expressing "exemplifies a group". This links to the
page defining a group, from which students can remember the precise
definition of a group and see other examples.

Can you tell me what sort of formalization is possible, and what
pedagogical advantage it would give, related to this specific
example? I think I'm having trouble imagining the pedagogical impact
of formalization.

best,

Marty

[nrolland]

Hi Marty,

The point is that if a system can do formal substitution and navigate
up and down a level of abstraction, then authors might collaborate and
reuse each others proofs (in their generality or reduced for a
specific case)

I feel like this aspect is essential if we want to describe maths in
an exhaustive way.
Essentially because it is in the presentation of math notions to a
specific audience that most of the variability resides, not in the
core mathematical objects, on which most people agree on.
Therefore we should clearly separate those, just like we separate
presentation and content in any modern software.
It is only sufficient to pick a random math subject and see the
numerous books that exists on it to justify the split.


The added value in the case of simply applying a definition is low..
but even so I guess for more abstract notion like category or functors
it can be useful.

For a complex proof, the ability to fold and unfold to a more basic
definition is key for the reader's comprehension. For instance, if I
read a proof using a synthetic argument (eg "because it is a hilbert
space, the minimun is reached") I might want to know how it is a
hilbert (may be its norm satisfies the parallelogram identity ?) and
how that implies the result (by the fact that the space is uniformly
convex, hence reflexive, hence....)
Yet I do not want to go too much in detail, as I probably do not want
not be bugged by proofs that a finite intersection of open set is
indeed open. But, who knows, at some point I or someone else will want
to for a split second.
From my math learning experience both cases of under or over detailed
proofs leads to wasted time understanding why an assertion is true, or
in "refactoring" the proof to extract the big movement out of a deluge
of trivialities.


I guess this sounds like wishful thinking and I would be glad to help
with my limited means if anything comes around..


regards,
Nicolas

> > > > > If you would like to take a look, I would certainly enjoy hearing...
>
> read more »