When in high school I was intrigued by proofs in geometry and later trig. As an experiment I tried to write proofs in J notation. Not too hard using explicit notation by converting the "traditional" notation to J. And I have seen where Ken verified steps of a proof by executing them with test data.
More fun to try to do it using tacit expressions. One toy I tried without too much success is: (+*-) -: ((-&*:) I wanted to do it without using any explicit expressions. And once done, perhaps there is a way to automate the process - write a script to do it. Has anyone else tried to do this? ---------------------------------------------------------------------- For information about J forums see http://www.jsoftware.com/forums.htm