Re: [isabelle] Any fans of "try"?
This is amazing and shows that we are nearly able to do experimental mathematics.
In fact, I have used nitpick in some tricky combinatorial proofs to check corner cases. It was very effective.
> On 26 May 2020, at 14:36, John F. Hughes <jfh at cs.brown.edu> wrote:
> Another note in praise of nitpick: in doing some work in synthetic affine
> and projective geometry, I wanted to exhibit a four-point affine plane. To
> do so required writing out the incidence relation (which points are on
> which lines), which was a case-by-case nightmare to write and read. But
> when instead I asked "try" to prove the theorem that every affine plane
> contains at least 5 points, nitpick instantly generated the standard
> 4-point affine plane for me. That's kind of a backwards approach, but it
> was, as I say, very useful.
This archive was generated by a fusion of
Pipermail (Mailman edition) and