FDL notes - DL scenarios2

Glossary FDLnotes

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
Continued from Scenarios of FDL Use

7
A mathematician wants to publish the definitive verified version of some tricky or tedious proof, making every detail available to the reader on demand. This mathematician finds that there are already proofs in the right style with the right mathematical basis, and finds not only the originator of the theorem, but also a reference to the "technical" creator. The mathematician is not proficient in the actual production of formally verifiable proofs, or at least not with the system he wants used, and so contracts the discovered "formal technician" to formalize his proof and have it posted to the FDL.

8
A person embarking on a formalization wants some ideas about how to start. They search for all theorems pertaining to a similar topic, and collect them for comparison. At best, someone has already made an adequate formulation, as demonstrated by the the elegance of the proofs that use those formulations. At second best, there are examples that are unsatisfactory, and so need not be re-attempted.

9
A formal proof technician wants to experiment with an unfamiliar logic used by another group, but does not want to have to learn the interface they use. Fortunately, the preparation system she normally uses has been interfaced to the FDL, and so has that of the other group. This means that the content and inference engines of the other group are accessible from her usual interface.

10a
A crank finds that he can never get his proofs to check with any of the logics everyone else seems to be using. People ignore his proofs because he introduced proof methods they have not become interested in.

10b
An amateur (or crank) manages to write a couple of proofs that do adhere to standards of proof widely used in the FDL, and one day while doing a formal search for lemmas useful in a new proof a mathematician comes across them and finds they are useful. It's okay that the person who wrote the proofs is an amateur (or crank).

11
A person who has developed or read a fair amount of material finds that a handful of authors are heavily represented among the FDL documents she uses, the lemmas cited, and programs incorporated. She then decides to survey all the material posted by any of the handful and has a process regularly advise her when new material is posted by those authors.

12a
Many utilities are developed over time by various parties, for searching the FDL or allowing a user to modify and develop his content. These utilities are themselves contributions to the FDL, and can be employed and discussed.

12b
Data mining for patterns of inference: an interested party applies a procedure to an extant body of formal proofs in the FDL that attempts to identify repeatedly used patterns of inference that should be repackaged as lemmas, derived rules or tactics.

Continued at Scenarios of FDL Use(part 3) IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html

Glossary FDLnotes

7	A mathematician wants to publish the definitive verified version of some tricky or tedious proof, making every detail available to the reader on demand. This mathematician finds that there are already proofs in the right style with the right mathematical basis, and finds not only the originator of the theorem, but also a reference to the "technical" creator. The mathematician is not proficient in the actual production of formally verifiable proofs, or at least not with the system he wants used, and so contracts the discovered "formal technician" to formalize his proof and have it posted to the FDL.

8	A person embarking on a formalization wants some ideas about how to start. They search for all theorems pertaining to a similar topic, and collect them for comparison. At best, someone has already made an adequate formulation, as demonstrated by the the elegance of the proofs that use those formulations. At second best, there are examples that are unsatisfactory, and so need not be re-attempted.

9	A formal proof technician wants to experiment with an unfamiliar logic used by another group, but does not want to have to learn the interface they use. Fortunately, the preparation system she normally uses has been interfaced to the FDL, and so has that of the other group. This means that the content and inference engines of the other group are accessible from her usual interface.

10a	A crank finds that he can never get his proofs to check with any of the logics everyone else seems to be using. People ignore his proofs because he introduced proof methods they have not become interested in.

10b	An amateur (or crank) manages to write a couple of proofs that do adhere to standards of proof widely used in the FDL, and one day while doing a formal search for lemmas useful in a new proof a mathematician comes across them and finds they are useful. It's okay that the person who wrote the proofs is an amateur (or crank).

11	A person who has developed or read a fair amount of material finds that a handful of authors are heavily represented among the FDL documents she uses, the lemmas cited, and programs incorporated. She then decides to survey all the material posted by any of the handful and has a process regularly advise her when new material is posted by those authors.

12a	Many utilities are developed over time by various parties, for searching the FDL or allowing a user to modify and develop his content. These utilities are themselves contributions to the FDL, and can be employed and discussed.

12b	Data mining for patterns of inference: an interested party applies a procedure to an extant body of formal proofs in the FDL that attempts to identify repeatedly used patterns of inference that should be repackaged as lemmas, derived rules or tactics.