
Re: Formal Proof Language Example  HumanReadable?
Posted:
Jun 24, 2009 10:53 AM


slawekk wrote: > Yes, I can understand the meaning of the (assertion of) the theorem. > I think a good formal proof language has to have the following > features: > > 1. Be readable for people with general mathematical education, without > having the study the language. Readability is of course relative and > depends on the reader's experience. For some people a proof is > readable if it looks like Lisp. For most mathematicians though the > proof is readable if it looks similar to what they can see in a > standard journal. I think your syntax does have this feature. [...]
I looked at the _Binomial_coefficients_ example page at Formalpedia: < http://formalpedia.org/Binomial_coefficients >
I can guess some of what the notation means, but not all.
For example, why is there a 'k' as the first character of k.Binomial_coefficients.binom ?
Another thing I don't understand is the meaning of Arith.fact in "Theorem (binom_fact_thm)" .
Any help will be appreciated.
David Bernier

