Email Gateway (Aug 22 2022 at 16:32): Email Gateway (Aug 22 2022 at 16:32):From: Lawrence Paulson <lp15@cam.ac.uk>
An unusual entry by Lukas Bulwahn: three different proofs inspired by a Mathematics Stack Exchange page. Many thanks, Lukas!
Larry Paulson
https://www.isa-afp.org/entries/Falling_Factorial_Sum.html
This entry shows that the falling factorial of a sum can be computed with an expression using binomial coefficients and the falling factorial of its summands. The entry provides three different proofs: a combinatorial proof, an induction proof and an algebraic proof using the Vandermonde identity. The three formalizations try to follow their informal presentations from a Mathematics Stack Exchange page as close as possible. The induction and algebraic formalization end up to be very close to their informal presentation, whereas the combinatorial proof first requires the introduction of list interleavings, and significant more detail than its informal presentation.
Email Gateway (Aug 22 2022 at 16:32):From: j4n bur53 <janburse@fastmail.fm>
Significant more detail, but also less readability. The
archive entry is quite repellent. There is no 2-diemensional
rendering of formulas, as compared to MSE. The most text
occupies the copyright notice at the end.
Something has to change!
Lawrence Paulson schrieb:
Email Gateway (Aug 22 2022 at 16:33):From: Lukas Bulwahn <lukas.bulwahn@gmail.com>
Hi,
Concerning the combinatorial proof, this entry simply shows that this
proof from elementary combinatorics is clearly more explicit than its
textbook proofs. If you also compare the formalisations of other
elementary combinatorics with their textbook proofs, you will find
that they are similarly explicit. Hence, I have the conjecture that
textbook proofs from elementary combinatorics can be much more
implicit for human readers; theorem provers need much more guidance
despite all the automation and reasoning power we have gained and
achieved over the last few decades.
Concerning the induction and algebraic proof, readability in the pdf
might currently be an open issue, but I believe this can be addressed
with latex output notation. So far, we have not formalized much
combinatorics and nobody provides a dedicated notation for typical
functions in combinatorics, such as binomial, factorial, rising
factorial/pochhammer, falling factorial or Stirling numbers.
You are free to contribute a theory that provides proper setup for the
used notation, or extend and modify the provided theories in the entry
to improve its presentation.
Best regards,
Lukas
Email Gateway (Aug 22 2022 at 16:33):From: j4n bur53 <janburse@fastmail.fm>
Wasn't a critique ad Hominem, only somehow it
confuses me increasingly that there is a discrepancy
between modern math notation, in current practice,
and what you generate in the archive. The archive is
kind of a hybrid between a PDF article and what you
enter in jEdit when creating Isabelle/HOL theorems.
But I am not sure whether it gets best of both worlds
or only a weak common denominator. jEdit looks more
like programming code with its coloring.
But what are the unique selling propositions of
the PDF articles? I don't know the actual status quo,
is it at all possible to generate 2-dimensional
output? Like the output a CAS would easily generate
for mathematical formulas such as sums, integrals, etc..
with all the subscript, superscript, etc...
Lukas Bulwahn schrieb:
Email Gateway (Aug 22 2022 at 16:33):From: j4n bur53 <janburse@fastmail.fm>
A starting point could be this example here (Page 20):
http://sketis.net/wp-content/uploads/2016/03/Curry-Club_Mar-2016.pdf
Its nice to see that there is a "also have : : :" construct
in Isar, many proofs on MSE essential use such a reasoning
sequence.
But nevertheless the stuff looks much better on MSE. Its
not only the 2-dimensional rendering, but also the use
of whitespace.
Here only a "Pedro" used induction:
https://math.stackexchange.com/a/34437/4414
But he didn't use the Sum sign, instead less symbolic notation,
with ellipses. For more advanced users you see Sum sign
usage although.
But then "Carlo"'s solution jump skips induction, and
the Sum sign and appeals goemetrically:
https://math.stackexchange.com/a/2263/4414
Quite fascinating. Should a PDF output drop some of
the Isar statements in favor of whitespace and 2-dimensional
rendering. How could this be done?
j4n bur53 schrieb:
Last updated: Nov 21 2024 at 12:39 UTC