I've slept since we had the thread about lemma concatenation. But this seems
relevant:
https://philpapers.org/rec/BARAHO-17?ref=mail
"In other words, if cumulative deductive progress is not guaranteed, we cannot
be sure that lemmas are knowledge checkpoints. But this seems quite an
important pr
It sounds like somebody back then found a pretty sweet gig.
--Barry
> On Mar 29, 2019, at 6:01 PM, Steven A Smith wrote:
>
> One interesting
> point was the clay-tablet records from Mesopotamia where algebraic
> solutions of (all?) quadratics and many cubics were enumerated, but
> redundantly
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 wit
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, i
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
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 p
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 jok
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 fir
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 o
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 pr
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
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 dependen
12 matches
Mail list logo
