Mr Boss Thanks for the interesting links.
On the subject of proof-assistants, you might be entertained by a little project I have been working at for some time, on and off. The aim is to produce a formal rigorous mathematical account of the semantics of the J programming language. Formality and rigor are ensured by using a widely-respected computer theorem-proving system. There are a number of these: Coq is one, as mentioned in the referenced article, but the one I like is the PVS system from SRI - see http://pvs.csl.sri.com/ Whether the result is about J or only about something similar to J would be a social process: my theorems are certainly true but would everyone agree that they are true of J? Have made only a very small beginning, with little theories (that is, definitions and some proved theorems) for nouns and and also for monadic and dyadic $ verb. Just to give a little of the flavor, here a short extract, about dyadic $ ========================================================= % the domain of Shape is a set of pairs of nouns (x,y) such that % if the product of x is nonzero then y is nonempty % A restriction is that x is currently limited to scalars or vectors. % This restriction is awaiting attention. SH : TYPE = {x, y:noun | (prodlist(atoms(x)) >0) implies (itemcount(y) > 0) } Shape (xy : SH) : noun = (dnn(xy`1, xy`2) , ann (xy) ) L29: LEMMA Shape(sa,sa) = va % 0 $ 0 is empty vector % sa is scalar zero % va is empty vector %|- L29: PROOF (grind) QED ============================================================== There is more stuff at http://www.learningj/THEORIES.ZIP Regards On Wed, Apr 13, 2016 at 9:40 PM, R.E. Boss <[email protected]> wrote: > > From: Chat [mailto:[email protected]] On Behalf Of 'Jon > > Hough' via Chat > > Sent: woensdag 13 april 2016 16:26 > > > > Slightly off-topic, but also a little on-topic, your post reminded me of > a slightly > > old article > > http://www.wired.com/2015/05/will-computers-redefine-roots-math/ > > about the use of coq, and other proof helpers, by mathematicians. It > seems > > computer aided proofs are going to become more important. > > I read the article, not that old btw, in Quanta Magazine and was amazed > that (the name of) Zeilberger was not mentioned, who is very outspoken on > this subject. > Read his http://www.math.rutgers.edu/~zeilberg/Opinion149.html where he > reminded that AlphaGo invented strategies unknown by the top world > Go-players in its games with the world champion. > He is convinced, and so am I, that computers, robots if you will, come up > with math we people hardly will understand. > And so will happen for other parts of science, art and life. > (this is chat anyway) > > > R.E. Boss > ---------------------------------------------------------------------- > For information about J forums see http://www.jsoftware.com/forums.htm ---------------------------------------------------------------------- For information about J forums see http://www.jsoftware.com/forums.htm
