That makes a lot of sense to me. I suppose my reaction (regarding misapplication of algorithms) has to do with something like "coherence-invariant composition" ... some sub-concept of truth-preservation through manipulation. Practically, it shows up in the (I claim false) distinction between validation (that some analog *behaves* similar to a referent) versus verification (that some analog/machine is constructed the way you *think* it's constructed).
My sense of formal math proofs always triggered my "So what?" homunculus. Sure, you can set up any game you want, then play that game. But the deeply interesting progressions in (my incompetent understanding of) math always came with the feeling they were *violating* some (unnecessarily) assumed rule somewhere. Projects *like* TheoremDep (not claiming that is The One) might help suss out lineages of reasoning that can both inhibit or facilitate a progressive step. It would be cool to see an interactive visualization of the ConcepDAG where a given lemma could be "turned off" and watch the progression of downstream conclusions also turn off or go away. I can imagine *if* the whole of math could be rendered in such a way, things like the fundamentals of math would reveal themselves to be more linear/chain-like, tree-like, or even more of an intertwined mesh. Turning off one lemma might make it more obvious that this lemma (or its particular form) is not on the "critical path" toward some practical/applied outcome downstream. Etc. But if actual mathematicians don't see anything like what I see in projects like this, then it's just more of my apophenia. On 3/28/19 6:44 AM, Barry MacKichan wrote: > I’ll comment with a story. Really, did you expect me to answer a question > with another question? > > Andrew Gleason was one of my favorite professors, and the solver of (one > interpretation of) Hilbert’s 5th problem. At one time, I checked out his > proof. It was hopeless. The statement that he was proving was not at all the > same as Hilbert’s problem; rather it was the proof of the last remaining > unproved lemma in a proof outline somewhere. > The theorem dependency project has the potential of documenting, at least, > the trail that leads to the final proof. In many cases, the only way to > understand, even superficially, such a trail is to start at the beginning. > What I had tried was to get on the trail from the side. > > --Barry > > On 27 Mar 2019, at 17:11, glen∈ℂ wrote: > >> Unfortunately, I have no sense of humor. (Seriously. I've been told so by >> many witty persons.) So, the question remains. Do you think that theorem >> dependency project is about concatenating proofs? >> >> On 3/27/19 2:02 PM, Frank Wimberly wrote: >>> Concatenate proofs. This reminds me of the old joke: >>> >>> 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. >>> >>>>> 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. -- ☣ 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-comic.blogspot.com/ by Dr. Strangelove
