<div dir="auto">Concatenate proofs. This reminds me of the old joke:<div dir="auto"><br></div><div dir="auto"><pre style="background:rgb(255,242,215);width:auto;border:solid rgb(249,223,173)">An Engineer walks in her office and finds her trash can on fire. She
gets the fire extinguisher and puts out the fire.
The Mathematician walks in his office and finds his trash can on fire.
He gets the fire extinguisher and puts out the fire.
The following day :
The Engineer walks in her office and finds the trash can on fire on
top of her desk. She gets the fire extinguisher and put out the fire.
The Mathematician walks in his office and finds the trash can on fire
on top of his desk. He takes the trash can and puts it on the floor.
He has reduced the problem to a previously solved state. Too solve it
again would be redundant.</pre><br><div data-smartmail="gmail_signature" dir="auto">-----------------------------------<br>Frank Wimberly<br><br>My memoir:<br><a href="https://www.amazon.com/author/frankwimberly">https://www.amazon.com/author/frankwimberly</a><br><br>My scientific publications:<br><a href="https://www.researchgate.net/profile/Frank_Wimberly2">https://www.researchgate.net/profile/Frank_Wimberly2</a><br><br>Phone (505) 670-9918</div></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Wed, Mar 27, 2019, 2:50 PM glen∈ℂ <<a href="mailto:gepropella@gmail.com">gepropella@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">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.<br>
<br>
On 3/22/19 4:31 PM, Joe Spinden wrote:<br>
> Of course not. Not to mention that there are often several different proofs of any significant theorem.<br>
> <br>
> Joe<br>
> <br>
> <br>
> On 3/22/19 3:54 PM, Frank Wimberly wrote:<br>
>> 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.<br>
>><br>
>> -----------------------------------<br>
>> Frank Wimberly<br>
>><br>
>> My memoir:<br>
>> <a href="https://www.amazon.com/author/frankwimberly" rel="noreferrer noreferrer" target="_blank">https://www.amazon.com/author/frankwimberly</a><br>
>><br>
>> My scientific publications:<br>
>> <a href="https://www.researchgate.net/profile/Frank_Wimberly2" rel="noreferrer noreferrer" target="_blank">https://www.researchgate.net/profile/Frank_Wimberly2</a><br>
>><br>
>> Phone (505) 670-9918<br>
>><br>
>> On Fri, Mar 22, 2019, 12:18 PM uǝlƃ ☣ <<a href="mailto:gepropella@gmail.com" target="_blank" rel="noreferrer">gepropella@gmail.com</a> <mailto:<a href="mailto:gepropella@gmail.com" target="_blank" rel="noreferrer">gepropella@gmail.com</a>>> wrote:<br>
>><br>
>><br>
>> I saw this on reddit this morning and thought some of you might<br>
>> like it:<br>
>><br>
>> <a href="https://sharmaeklavya2.github.io/theoremdep/" rel="noreferrer noreferrer" target="_blank">https://sharmaeklavya2.github.io/theoremdep/</a><br>
>> > Track dependencies between theorems.<br>
>><br>
>> > About TheoremDep<br>
>> > TheoremDep contains many theorems and shows you the dependencies<br>
>> for each theorem. Theorem X is said to be dependent on theorem Y<br>
>> iff Y is used as a lemma in the proof of X. Therefore, this<br>
>> website presents proofs in a way which simultaneously achieves the<br>
>> goals of not assuming any prior knowledge and making it easy to<br>
>> skip parts you already know.<br>
>> ><br>
>> > TheoremDep is generated using ConcepDAG. ConcepDAG is a tool to<br>
>> visualize dependencies between things in the form of a static website.<br>
>> ><br>
>> > If you want to contribute, check out the source code of these<br>
>> projects:<br>
>> ><br>
>> > TheoremDep<br>
>> > ConcepDAG<br>
>><br>
>><br>
>><br>
>> -- ☣ uǝlƃ<br>
>><br>
>> ============================================================<br>
>> FRIAM Applied Complexity Group listserv<br>
>> Meets Fridays 9a-11:30 at cafe at St. John's College<br>
>> to unsubscribe <a href="http://redfish.com/mailman/listinfo/friam_redfish.com" rel="noreferrer noreferrer" target="_blank">http://redfish.com/mailman/listinfo/friam_redfish.com</a><br>
>> archives back to 2003: <a href="http://friam.471366.n2.nabble.com/" rel="noreferrer noreferrer" target="_blank">http://friam.471366.n2.nabble.com/</a><br>
>> FRIAM-COMIC <<a href="http://friam.471366.n2.nabble.com/FRIAM-COMIC" rel="noreferrer noreferrer" target="_blank">http://friam.471366.n2.nabble.com/FRIAM-COMIC</a>><br>
>> <a href="http://friam-comic.blogspot.com/" rel="noreferrer noreferrer" target="_blank">http://friam-comic.blogspot.com/</a> by Dr. Strangelove<br>
>><br>
>><br>
>> ============================================================<br>
>> FRIAM Applied Complexity Group listserv<br>
>> Meets Fridays 9a-11:30 at cafe at St. John's College<br>
>> to unsubscribe <a href="http://redfish.com/mailman/listinfo/friam_redfish.com" rel="noreferrer noreferrer" target="_blank">http://redfish.com/mailman/listinfo/friam_redfish.com</a><br>
>> archives back to 2003: <a href="http://friam.471366.n2.nabble.com/" rel="noreferrer noreferrer" target="_blank">http://friam.471366.n2.nabble.com/</a><br>
>> FRIAM-COMIC <a href="http://friam-comic.blogspot.com/" rel="noreferrer noreferrer" target="_blank">http://friam-comic.blogspot.com/</a> by Dr. Strangelove<br>
> <br>
> <br>
> ============================================================<br>
> FRIAM Applied Complexity Group listserv<br>
> Meets Fridays 9a-11:30 at cafe at St. John's College<br>
> to unsubscribe <a href="http://redfish.com/mailman/listinfo/friam_redfish.com" rel="noreferrer noreferrer" target="_blank">http://redfish.com/mailman/listinfo/friam_redfish.com</a><br>
> archives back to 2003: <a href="http://friam.471366.n2.nabble.com/" rel="noreferrer noreferrer" target="_blank">http://friam.471366.n2.nabble.com/</a><br>
> FRIAM-COMIC <a href="http://friam-comic.blogspot.com/" rel="noreferrer noreferrer" target="_blank">http://friam-comic.blogspot.com/</a> by Dr. Strangelove<br>
> <br>
<br>
============================================================<br>
FRIAM Applied Complexity Group listserv<br>
Meets Fridays 9a-11:30 at cafe at St. John's College<br>
to unsubscribe <a href="http://redfish.com/mailman/listinfo/friam_redfish.com" rel="noreferrer noreferrer" target="_blank">http://redfish.com/mailman/listinfo/friam_redfish.com</a><br>
archives back to 2003: <a href="http://friam.471366.n2.nabble.com/FRIAM-COMIC" rel="noreferrer noreferrer" target="_blank">http://friam.471366.n2.nabble.com/<br>
FRIAM-COMIC</a> <a href="http://friam-comic.blogspot.com/" rel="noreferrer noreferrer" target="_blank">http://friam-comic.blogspot.com/</a> by Dr. Strangelove<br>
</blockquote></div>