Skip to content
Automated Reasoning for the Working Mathematician
Isabelle
Branch: master
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
isabelle_experiments
README.md
feedback.md

README.md

Automated Reasoning for the Working Mathematician

I set up this repository to help me prepare a talk for FroCoS / Tableaux in September 2019. The current draft of the talk is here:

http://www.andrew.cmu.edu/user/avigad/Talks/london.pdf

Some preliminary notes are here:

http://www.andrew.cmu.edu/user/avigad/Papers/arwm_notes.pdf

(Warning: they are wordy.)

After preparing the notes, I asked friends and colleagues to respond to the questions below. You can find some of their responses on Issue #1 in this repository. Some additional feedback is summarized in feedback.md.

The directory isabelle_experiments provides some experiments using automation with Isabelle, with notes.

I intend to keep this repository publicly available, in case it is useful to anyone.

Questions

If you have done any substantial formalization of mathematics, I would like to know:

  • What kinds of automation have you found helpful?
  • What kinds of automation do you think would be helpful?

Even a quick, short response will be appreciated, and if you don't think automation is useful or necessary, you can say so. If you can point to particular examples where automated tools proved useful, or particular examples of inferences that were painful to justify by hand, that would be especially helpful.

You can post an answer as a comment to Issue #1 in this repository. (The public meant to encourage discussion, so that is welcome, too.) You can also write me privately at avigad@cmu.edu.

Feel free to share this request with anyone who may be interested.

You can’t perform that action at this time.