Week 32 - 2021

The weeknote for 8/9 - 8/15.

History

Been reading a little about modern Chinese History (around 1920 - 1940). I was a little bit surprised by the fact that the founders of the modern China, Sun Yat-sen and Chiang Kai-shek, both had experience of living in Japan. Sun Yat-sen even take his later name 中山 from Japanese family name. I feel this partially describes why the Taiwanese people are often pro-Japanese.

I also read about Manchurian incident, especially Liutiao Lake incident. This event is now understood as a false flag event by Japanese army. However probably this event had been advertised as Chienese attack by the Japanese government at the time during the war. I'd like to dig deeper about this in the future, like when the public understanding of this event was changed and 'fixed' in the history.

We had somen noodle on Wednesday. Somen is cold noodle, which is very good for summer season.

#kt3kmeal 今日はそうめん pic.twitter.com/QuRSrTb7g6
— Yoshiya Hinosawa (@kt3k) August 11, 2021

Iyo-chan and I went to a ramen restaurant, Rakkan, in Roppongi, Tokyo. It was a nice place and the ramen tasted delicious. The food itself was very delicious, but I was more impressed by their tableware, interior, and atmosphere of the shop itself.

#kt3kmeal 楽観, Roppongi pic.twitter.com/x22McvJNFI
— Yoshiya Hinosawa (@kt3k) August 14, 2021

These days I've been reading about the connection between typed lambda calculus, cartesian closed category, and deductive systems. Mathematicians say these 3 different mathematical systems are the same! That sounds really fascinating. However I still haven't got the details about this claim. Especially the definition of cartesian closed cateogry looks extremely difficult to me (Deductive systems and typed lambda calculi look a little less difficult compared to that).

The fundamental purpose of this reading is to find out the correct language for my project, in which I aim to provide the toolset for working on completely formal proofs of mathematical theorems (typically Wiedijk's 100 theorems), which should be more comfortable than the existing ones such as HOL family, Coq, Isabelle, Lean, Mizar, Metamath, Idris, Twelf.

The existing theorem proovers like the above all look terrible to me. The main reason is that the proofs in these systems never look like 'a proof' to me. In my view, 'a proof' has to make the reader of it understand the claim, and force them believe the claim because of its logical correctness. None of the above systems provides the proof in this sense. So if a proof is written in my system, it'll be easy for humans to read without (much) foreknowledge about the system (at least the necessary foreknowledge all be written down somehow). You can work on this system in a very similar way to the way which you usually do in the blackboard.