drchewbacca
Joined 7 years ago
Joined 7 years ago
It would be possible to make something pretty cool out of the database I think.
Here is the main site. http://us.metamath.org/index.html
Here is the book which can help with understanding. http://us.metamath.org/downloads/metamath.pdf
Here are some tutorials for MMJ2 which is the main proof assistant to use, https://www.youtube.com/playlist?list=PL1jSu6GGefBm7RBP0Id2S...
it can be found here, http://us.metamath.org/#mmj2
Here are some beginners proof exercises which are a good place to start out
http://us.metamath.org/mpegif/mmtheorems289.html#mm28844b
I will warn you though it is a bit like the wild west, it is not easy to accomplish anything and it is exciting to be on the frontier.
The community is really cool, you can chat with them here.
So questions around statements which are true but not provable in certain logical systems do have concrete examples and are interesting imo.
https://math.stackexchange.com/questions/625223/do-we-know-i...
"On April 17, 2013, Yitang Zhang announced a proof that for some integer N that is less than 70 million, there are infinitely many pairs of primes that differ by N."
For example it is proven there are infinitely many primes. Are there infinitely primes that differ by 2? By n for any n? Are there infinitely many palindromic primes? Are there infinitely many primes of form n^2 + 1? Is there always a prime between n^2 and (n+1)^2?
If this is true then, assuming there are 200k proven theorems, there would be >1m unproven but readily stated theorems which would mean it wouldn't be too hard to find areas no one is looking into.
I might be wrong though.
"If the schedule is long it's wrong, if it's tight it's right. The best part is no part, the best process is no process."
All the hacking away of parts and processes pays off with speed.
https://en.wikipedia.org/wiki/English_claims_to_the_French_t...
I would imagine that if we really cared about climate change the best approach would be maximal effort on all fronts. So build renewables as fast as we can and build nuclear as fast as we can. That would be the quickest way to get carbon emissions to 0.
We could always spend the latter half of the century decommissioning the nuclear again.
‘Question: ... Two top grandmasters have gone down to chess computers: Portisch against “Leonardo” and Larsen against “Deep Thought”. It is well known that you have strong views on this subject. Will a computer be world champion, one day ...?
Kasparov: Ridiculous! A machine will always remain a machine, that is to say a tool to help the player work and prepare. Never shall I be beaten by a machine! Never will a program be invented which surpasses human intelligence. And when I say intelligence, I also mean intuition and imagination. Can you see a machine writing a novel or poetry? Better still, can you imagine a machine conducting this interview instead of you? With me replying to its questions?’
Of course it might lead to living to 800 and being confined to a wheelchair by 80.
If you gave me a book of inverse kinematics I'd go to sleep in 10 minutes. If I get frustrated that my robot keeps falling over I could read about it for days.