On Jun 24, 10:53 am, David Bernier <david...@videotron.ca> wrote: > 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)" .
This is an example what happens when the proof language does not satisfy the "readability by mathematician" criterion. I can only guess that the k.Binomial_coefficients.binom string there sets up the context so that \forall k really means \forall k \in N , where N is the set (type?) of natural numbers. I believe that any system based on type theory (rather than set theory) will be difficult to read for an average mathematician. Standard mathematics is based on set theory and proof languages based on type theory must have additional notation for indicating types. For example, Isabelle's Isar is very readable when used with ZF logic, but much less so when used with HOL, with all that "`a" and "::" noise in the notation.