TheoremDep
Locked
 
|
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-comic.blogspot.com/ by Dr. Strangelove
uǝʃƃ ⊥ glen
|
|
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ƃ ☣ <[hidden email]> wrote:
============================================================ 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 |
|
|
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:
-- Joe Confidentiality Notice: This e-mail communication and any attachments may contain confidential and privileged information for the use of the designated recipients named above. If you are not the intended recipient, you are hereby notified that you have received this communication in error and that any review, disclosure, dissemination, distribution, or copying of it or its contents is prohibited. If you have received this communication in error, please notify me immediately by replying to this message and deleting it from your computer. Thank you. ============================================================ 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 |
|
|
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ƃ ☣ <[hidden email] <mailto:[hidden email]>> 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
uǝʃƃ ⊥ glen
|
|
|
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. ----------------------------------- 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 Wed, Mar 27, 2019, 2:50 PM glen∈ℂ <[hidden email]> wrote: 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. ============================================================ 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 |
|
|
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. ============================================================ 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
uǝʃƃ ⊥ glen
|
|
|
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. > > ============================================================ > 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 |
|
|
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
uǝʃƃ ⊥ glen
|
|
|
Glen- Sorry I didn't respond to this sooner... I had a hard time "getting around to" exploring TheoremDep (and ConcepDag) enough to comment (meaningfully?). All I think Frank and Joe did was make a jump from TheoremDep the tool to imagining things one might do with the underlying ConcepDag data structure... "proof generation" I suppose. I have my own "so what" homunculus. I have a BS in Math but definitely recognized that I would never be a "Mathematician". I appreciate the spirit and perspective of *real Mathematicians* and (sometimes) even respect their contributions when they are driven by curiosity or "because it is there" which sometimes anticipates the practical needs of Engineering and Science. The old fascination with why mathematics (as a pure abstraction) seems to line up so well with physical reality comes up again. I think there is some kind of anthropic principle involved? Do you have any parallax on this? I would *also* like to try to lay out the ConceptDAG data structure with enough interactivity to do as you suggest ... removing a node and seeing what "breaks"... or possibly adjusting weights on the edges? I'm not clear there is a meaningful semantic to that, but as usual I'm interested in trying to get a "big picture". I did a project like this with the Gene Ontology in 2004 or so...
The Gene Ontology is a partially
ordered set which provided more constraints (and opportunities)...
in this example, we didn't delete individual nodes, but could
adjust the force-directed layout paramaters as well as grab any
node and drag it far from it's equilibrium position. This was
useful for untangling local energy minima but also for inferring
dependencies.
- Steve ============================================================ 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 |
|
|
On 3/29/19 9:29 AM, Steven A Smith wrote: > All I think Frank and Joe did was make a jump from TheoremDep the tool to imagining things one might do with the underlying ConcepDag data structure... "proof generation" I suppose. Yes, I can see that. The answer(s) to the question, though, is still interesting. I tried to allude to it by offering the 3 alternatives: chain, tree, mesh from the foundations up to "sophisticated" conclusions. It seems to me that if one reacts to something like TheoremDep with a sense of "concatenation", then that implies they think about this sort of reasoning as a chain or, at least, a tree. For context, I have the same problem with what we've (I've?) come to call "physics-based biological modelers". Their focus is on physically realistic simulation engines, upon which they implement chemically realistic reactions, upon which they implement biologically realistic mechanisms. I (being the soft-X type of person I am), tend to focus on *relational* modeling, which can be usefully applied at any layer of the heterarchy. Or, at least, I prefer a "middle out" method, starting at the layer where you understand/care the most. The physics-based people tend to think in terms of chains and trees, whereas the relational people tend to think in terms of networks. I call the phyics-based people "Grand Unified Modelers" because they're seeking the One True Model. ... very Monistic. > The old fascination with why mathematics (as a pure abstraction) seems to line up so well with physical reality comes up again. I think there is some kind of anthropic principle involved? Do you have any parallax on this? I tend to believe it boils down to *attention*, intentionality, purposeful behavior. It strikes me that math can unambiguously describe *anything*, real or fantasy. And where non-ambiguity is required, math will be successful. Bands like Tool argue against me in some sense, because they use a lot of math in the creative composition of their tunes and lyrics. But, then again, they're nerds and have high expectations for how tightly a performance hangs together ... which is, again, a requirement for non-ambiguity. My guess is math would be less successful if we tried to use it to, say, foster creativity in children ... at least for now. > I would *also* like to try to lay out the ConceptDAG data structure with enough interactivity to do as you suggest ... removing a node and seeing what "breaks"... or possibly adjusting weights on the edges? I'm not clear there is a meaningful semantic to that, but as usual I'm interested in trying to get a "big picture". I did a project like this with the Gene Ontology in 2004 or so... Very nice! Thanks for including the graphs. > The Gene Ontology is a partially ordered set which provided more constraints (and opportunities)... in this example, we didn't delete individual nodes, but could adjust the force-directed layout paramaters as well as grab any node and drag it far from it's equilibrium position. This was useful for untangling local energy minima but also for inferring dependencies. The author of TheoremDep cites Metacademy (here's a good example: https://metacademy.org/graphs/concepts/incompleteness_of_set_theory#focus=mh2y5zs9&mode=explore). That strikes me as a system amenable to edge weight adjustment. E.g. How important is it to understand Russell's Paradox, really, for understanding how ZF fits into this "lineage of reasoning"? In the kind of graph I'm imagining, it may be better to imagine the lemmas as edges and the nodes as something else (conceptions of reality, maybe?). Lemmas would, then, be transitions from one state to another. -- ☣ 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
uǝʃƃ ⊥ glen
|
|
|
Glen -
> Yes, I can see that. The answer(s) to the question, though, is still interesting. I tried to allude to it by offering the 3 alternatives: chain, tree, mesh from the foundations up to "sophisticated" conclusions. It seems to me that if one reacts to something like TheoremDep with a sense of "concatenation", then that implies they think about this sort of reasoning as a chain or, at least, a tree. Reading ahead, I want to respond to this with anticipation toward what you write in the next paragraph. When I first saw the TheoremDep, I thought of a tree which is pretty close to a DAG because of the obvious constraint that we don't want circular dependencies/logic in our proofs. I didn't think of concatenation as much as composition. In principle, one could unroll or serialize all the dependencies of a theorem and include them in the proof. I remember when I took a (belated?) course in the History of Mathematics near the end of my BS in math. I think I took it as credit toward a history course, though it was at least 2nd year math in some of it's content. One interesting point was the clay-tablet records from Mesopotamia where algebraic solutions of (all?) quadratics and many cubics were enumerated, but redundantly across different contexts, expressed as "story problems". It may not have been as bad as offering the same solution to determining crop yields for wheat and rye in separate story-problems, but less immediate abstractions/analogies would have been redundantly "solved". > For context, I have the same problem with what we've (I've?) come to call "physics-based biological modelers". Their focus is on physically realistic simulation engines, upon which they implement chemically realistic reactions, upon which they implement biologically realistic mechanisms. I think there is good motivation for believing that Chemistry "emerges" from physics and Biology "emerges from" Chemistry and Physics. At the same time, the point of emergent phenomena is that the governing "forces" between entities are NOT directly or obviously based in the next lower level of abstraction. So, while Metabolic Networks *DO* operate on Chemistry (and maybe some Physics like diffusion?), the governing logic IS relational, as you point out. Higher levels of abstraction like protein expression networks and (as my last example on Gene Ontologies represent) higher levels of abstraction have their own logic which "emerges" from the lower levels. > I (being the soft-X type of person I am), tend to focus on *relational* modeling, which can be usefully applied at any layer of the heterarchy. I think that is the *point* (if we need to invoke a Final Cause here) of these "layers" of emergent functionality. To support more and more complex types of relations (not just linear, heirarchical, etc.)... I haven't thought it through well, but I'm guessing that (for example), metabolic networks, or gene expression networks have a qualitative higher complexity than *most* physics phenomena (though Feynman diagrams describe "relations" between subatomic particles, and there MAY be known/interesting/relevant examples with similar complexity?) > Or, at least, I prefer a "middle out" method, starting at the layer where you understand/care the most. The physics-based people tend to think in terms of chains and trees, whereas the relational people tend to think in terms of networks. I call the phyics-based people "Grand Unified Modelers" because they're seeking the One True Model. ... very Monistic. I do believe that there is a conceit of Physics that if there is a place for a Monistic GUT it would be in Physics, but I think there is room for the same in Chemistry, Biology, Sociology, Economics, etc... within the domain circumscribed by the "floor and ceiling" of emergence(s)? >> The old fascination with why mathematics (as a pure abstraction) seems to line up so well with physical reality comes up again. I think there is some kind of anthropic principle involved? Do you have any parallax on this? > I tend to believe it boils down to *attention*, intentionality, purposeful behavior. It strikes me that math can unambiguously describe *anything*, real or fantasy. And where non-ambiguity is required, math will be successful. I think this is accurate, maybe tautological... > Bands like Tool argue against me in some sense, because they use a lot of math in the creative composition of their tunes and lyrics. But, then again, they're nerds and have high expectations for how tightly a performance hangs together ... which is, again, a requirement for non-ambiguity. I think the point in "interesting" endeavors is to provide enough familiar structure to be "familiar" and then add to (abberate?) it enough to be "surprising". > My guess is math would be less successful if we tried to use it to, say, foster creativity in children ... at least for now. I would claim that more than a little of my own personal creativity was based IN mathematics as a child/adolescent. It was the abstract language of math that allowed me to see (and manipulate?) patterns across more disparate domains than "natural language" allowed. It wasn't the lack of ambiguity (because my clumsy application re-indroduced ambiguity) in Math that drew me, but the ease and expressiveness of abstraction. > The author of TheoremDep cites Metacademy (here's a good example: https://metacademy.org/graphs/concepts/incompleteness_of_set_theory#focus=mh2y5zs9&mode=explore). That strikes me as a system amenable to edge weight adjustment. E.g. How important is it to understand Russell's Paradox, really, for understanding how ZF fits into this "lineage of reasoning"? I am working on a project involving the quantification and visualization of uncertainty. In that it is implicit that we want to propogate uncertainty through many different processes or models or scenarios. It seems somewhat to be a parallel to what you describe here around MetAcademy. > the kind of graph I'm imagining, it may be better to imagine the lemmas as edges and the nodes as something else (conceptions of reality, maybe?). Lemmas would, then, be transitions from one state to another. I do see the (potential) value of considering this "dual" of the dependency graph... a Lemma as you say, can be considered a transition from one state of knowledge or conviction or proof to another state. - Steve > ============================================================ 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 |
|
|
It sounds like somebody back then found a pretty sweet gig.
--Barry > On Mar 29, 2019, at 6:01 PM, Steven A Smith <[hidden email]> wrote: > > One interesting > point was the clay-tablet records from Mesopotamia where algebraic > solutions of (all?) quadratics and many cubics were enumerated, but > redundantly across different contexts, expressed as "story problems". ============================================================ 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 |
|
|
In reply to this post by Steve Smith
There's a lot to respond to, as always. But, also as always, I'm most attracted to potential conflict. 8^) And I'm going to be offensive and claim to know you better than you know yourself. >8^D
I'd argue that your personal creativity as a kid wasn't based in math, but based in something more concrete like your physiology and brain wiring. The math simply turned out to facilitate whatever twitch you'd already manifested. I'll try to use my go-to anecdote to make my point clearer. As a kid, my dad consistently accused me of "making excuses" in stead of "providing reasons". He saw some non-ambiguity in the (social) world that I never saw (still don't see to this day). Had he been more *logically* inclined, he might have been able to make the distinction clear to me. After I learned some of the concepts from control theory, I began to realize he (as a former drill sergeant and practicing Catholic) understood personal responsibility as a very interactive, dynamically controlled, always on the lookout, theistic, process. I tend to be a bit more essentialist and look for critical paths, shaving off the parts of the system that may have less (or negligible) impact on the particular outcome of interest/conflict. This intolerance for ambiguity, in me, manifested VERY early. From my incompetent understanding of pop-psy like "All I really Need to Know, I Learned in Kindergarten", my guess is math facilitated your innate creativity as opposed to *founding/basing* your creativity. But my claim that math would be less successful describing creativity in children than it is in, say, estimating the mass of ultra diffuse galaxies, has more to do with the ambiguity (distinct from uncertainty) in how we understand children. I suspect you would temporarily abide the claim that a nerd kid who spends all her time playing video games can be just as creative as a more artsy kid who spends her time making up songs on a keyboard. If we were talking about *adults*, it would be trivial to parse out, disambiguate, how one can be just as creative as another. But because our understanding of development is so impoverished, it can be difficult to *model* how a child meshes with (relaxes into) the control surface of a keyboard versus that of a game console. It's not really because "creativity" is ill-defined. It's because "children" is ill-defined. Creativity can (and has been) disambiguated in various (inconsistent[†]) ways by various researchers. We've seen less success disambiguating children. [†] And, contrary to popular belief, math allows for inconsistency. On 3/29/19 3:01 PM, Steven A Smith wrote: > I would claim that more than a little of my own personal creativity was > based IN mathematics as a child/adolescent. It was the abstract > language of math that allowed me to see (and manipulate?) patterns > across more disparate domains than "natural language" allowed. It > wasn't the lack of ambiguity (because my clumsy application > re-indroduced ambiguity) in Math that drew me, but the ease and > expressiveness of abstraction. ============================================================ 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
uǝʃƃ ⊥ glen
|
«
Return to Friam
|
1 view|%1 views
| Free forum by Nabble | Edit this page |