It's not clear to me that the intent of that dependency project is to
concatenate proofs. Is that what you guys think it's purpose is? It seems, to
me, more like a reliability analysis, where the trustworthiness of any
component depends (to a greater or lesser) extent on the trustworthiness of its
parts ... weakest link of the (inferential) chain and all that. I've seen the
misapplication of various numerical solutions throughout my career. And one of
the important aspects of applying any given algorithm is the assurance that its
inputs satisfy whatever requirements/assumptions are necessary for the output
to be trustworthy. This seems similar.
On 3/22/19 4:31 PM, Joe Spinden wrote:
Of course not. Not to mention that there are often several different proofs of
any significant theorem.
Joe
On 3/22/19 3:54 PM, Frank Wimberly wrote:
I can see that the proof of a theorem can be constructed by concatenating
proofs of theorems that it depends on but I wonder if that would produce the
most succinct and comprehensible proof.
-----------------------------------
Frank Wimberly
My memoir:
https://www.amazon.com/author/frankwimberly
My scientific publications:
https://www.researchgate.net/profile/Frank_Wimberly2
Phone (505) 670-9918
On Fri, Mar 22, 2019, 12:18 PM uǝlƃ ☣ <geprope...@gmail.com
<mailto:geprope...@gmail.com>> wrote:
I saw this on reddit this morning and thought some of you might
like it:
https://sharmaeklavya2.github.io/theoremdep/
> Track dependencies between theorems.
> About TheoremDep
> TheoremDep contains many theorems and shows you the dependencies
for each theorem. Theorem X is said to be dependent on theorem Y
iff Y is used as a lemma in the proof of X. Therefore, this
website presents proofs in a way which simultaneously achieves the
goals of not assuming any prior knowledge and making it easy to
skip parts you already know.
>
> TheoremDep is generated using ConcepDAG. ConcepDAG is a tool to
visualize dependencies between things in the form of a static website.
>
> If you want to contribute, check out the source code of these
projects:
>
> TheoremDep
> ConcepDAG
-- ☣ uǝlƃ
============================================================
FRIAM Applied Complexity Group listserv
Meets Fridays 9a-11:30 at cafe at St. John's College
to unsubscribe http://redfish.com/mailman/listinfo/friam_redfish.com
archives back to 2003: http://friam.471366.n2.nabble.com/
FRIAM-COMIC <http://friam.471366.n2.nabble.com/FRIAM-COMIC>
http://friam-comic.blogspot.com/ by Dr. Strangelove
============================================================
FRIAM Applied Complexity Group listserv
Meets Fridays 9a-11:30 at cafe at St. John's College
to unsubscribe http://redfish.com/mailman/listinfo/friam_redfish.com
archives back to 2003: http://friam.471366.n2.nabble.com/
FRIAM-COMIC http://friam-comic.blogspot.com/ by Dr. Strangelove
============================================================
FRIAM Applied Complexity Group listserv
Meets Fridays 9a-11:30 at cafe at St. John's College
to unsubscribe http://redfish.com/mailman/listinfo/friam_redfish.com
archives back to 2003: http://friam.471366.n2.nabble.com/
FRIAM-COMIC http://friam-comic.blogspot.com/ by Dr. Strangelove
============================================================
FRIAM Applied Complexity Group listserv
Meets Fridays 9a-11:30 at cafe at St. John's College
to unsubscribe http://redfish.com/mailman/listinfo/friam_redfish.com
archives back to 2003: http://friam.471366.n2.nabble.com/
FRIAM-COMIC http://friam-comic.blogspot.com/ by Dr. Strangelove
