Journal home page General information Submit an item Download style files Copyright Contact us

TeX files are text files which are readable by other programs. Mathematical proofs written using TeX can be checked by a Python program provided they are expressed in a sufficiently strict proof language. Such a language can be constructed using only a few extensions beyond the syntax of Morse's book, one being the incorporation of explicit theorem number references into the syntax. Such a program has been applied to and successfully checked the theorems in a significant initial segment of a book length mathematical manuscript.

Bob Neveln got his B.S. in mathematics from Caltech in 1967, (where he learned mathematical analysis from Don Knuth), and received his PhD from Northwestern University in 1976 for a dissertation on the formal language of A.P. Morse. Since 1987 he has held a joint appointment in mathematics and computer science at Widener University. He began using TeX (LaTeX) when he wrote Linux Assembly Language Programming which was published in 2000. He is a peace activist and met his wife, Buthaina Hawas, in Baghdad while there in January of 2003 with Academics for Peace. They now have a one year old boy, Ibraheem. Contact him at

Bob Alps received a Ph.D. in mathematics from Northwestern University in 1979. His field of study was definitions in Morse languages. Bob has worked as a pension consulting actuary for the Wyatt Company, Sedgwick Noble Lowndes, The Segal Company, and currently for Towers Perrin in Chicago. Bob currently serves as Examination General Officer for the Society of Actuaries examinations in probability and financial mathematics. Bob can be reached at or by phone at 312.201.5819.

PDF version of paper Comment on this paper Send submission idea to editor

Page generated June 9, 2010 ; TUG home page; join TUG/renew membership; webmaster; facebook; x; mastodon.