Email Gateway (Aug 19 2022 at 15:53): Email Gateway (Aug 19 2022 at 15:53):From: Gottfried Barrow <igbi@gmx.com>
Lee,
I assume you're working in Isabelle/HOL, with an entry point of
importing Complex_Main, and not extending HOL with any axioms of your own.
SHORT ANSWER PART 1: HOL is a logic, with a defined set of axioms (all
of which are not clearly made known to users in the Isabelle
literature), and as with mathematics in general, you are free to define
algebraic operations, but what you can or cannot prove is dependent on
your definitions, and on the HOL axioms.
SHORT ANSWER PART 2 (the global law of spheres of mathematical influence) :
a) In general, our proofs about math that are of interest to us, are of
no interest to others, and
b) if the math we're interested in is of no great, practical value, not
only are others not interested in any proofs about such math, they're
most likely not interested in the math.
SHORT ANSWER PART 3: Back to part 1, and with part 2 in mind, it's up to
you to show what can or cannot be done in Isabelle/HOL, for what hasn't
been done in Isabelle/HOL, for what you're interested in.
SHORT ANSWER PART 4: The above explains my approach, based on my past
observations of the culture of mathematics. But even big time players,
in all cultures, have a hard time getting people interested in what
they're doing. Google, with millions of dollars in funding, couldn't get
people very much interested in Google+, and as people got bored with
Myspace, they will most likely get bored with Facebook.
That's the short answer.
I'll leave off the long answer, involving my opinions about marketing,
and how marketing is generally necessary to draw people into what we are
doing, and what we are interested in.
Personally, what I have in mind is dance, trance, and disco, where the
disco will hopefully be kept to a minimum, especially the display of
gold chains, by means of leaving unbuttoned the top three buttons of a
yellow, polyester shirt.
But even trance can be risky. It's not that my professional reputation
can be tarnished, since I have no professional reputation. It's that if
one has heard 4 measures of trance, one has heard 4 hours of trance,
which we could rephrase as the Law of Trance, "If one has heard 4
measures of trance, one has heard 4 hours of trance."
Regards,
GB
Last updated: Apr 19 2024 at 20:15 UTC