Lean 4
I saw several Mastodon posts by Terence Tao recently on his learning journey with Lean 4 and used it for the formalization of his paper. He began his learning with Lean 4 from scratch on Oct. 9 [1] with the help of ChatGPT and completed the formalization on Nov. 5 [2]. It's always fascinating to see how differently the same tools can be used by such talented people. Some of his comments on ChatGPT in the past:
AI tools like #ChatGPT will soon be capable of answering a large fraction of traditional university homework type questions with reasonable accuracy. In the long term, it seems futile to fight against this; perhaps what we as lecturers need to do is to move to an "open books, open AI" mode of examination where we give the students full access to AI tools but ask them more challenging questions, both to teach the material and also to teach the students how best to use the AI tools of the future.
Dec 19, 2022, 16:21, https://mathstodon.xyz/@tao/109543141003492779
Today was the first day that I could definitively say that #GPT4 has saved me a significant amount of tedious work. As part of my responsibilities as chair of the ICM Structure Committee, I needed to gather various statistics on the speakers at the previous ICM (for instance, how many speakers there were for each section, taking into account that some speakers were jointly assigned to multiple sections). The raw data (involving about 200 speakers) was not available to me in spreadsheet form, but instead in a number of tables in web pages and PDFs. In the past I would have resigned myself to the tedious task of first manually entering the data into a spreadsheet and then looking up various spreadsheet functions to work out how to calculate exactly what I needed; but both tasks were easily accomplished in a few minutes by GPT4, and the process was even somewhat enjoyable (with the only tedious aspect being the cut-and-paste between the raw data, GPT4, and the spreadsheet).
Am now looking forward to native integration of AI into the various software tools that I use, so that even the cut-and-paste step can be omitted. (Just being able to resolve >90% of LaTeX compilation issues automatically would be wonderful...)
Apr 09, 2023, 20:37, https://mathstodon.xyz/@tao/110172426733603359
On the other hand, Lean 4 [3] is a very interesting project. Sure, Lean 4 can be learned by people from different perspectives [4]. I'm wondering how I can benefit from Lean 4 in the field of computer networking. I saw some ongoing projects such as SciLean [5] which is currently a proof-of-concept project on optimization and machine learning. Maybe it can be helpful in computer networking in term of algorithm formalization or to proof certain algorithm properties. Nonetheless, it should be "fun" to learn something completely new to me, maybe in 2024.
Cloud Computing in Africa
Somehow I needed a VPS running in Africa, specifically in Lagos, Nigeria. Currently, major cloud computing companies don't have a major market share in Africa and most of them are located in South Africa.
Google Cloud Platform:
Announced in Oct. 2022 [6], there will be a new region in Johannesburg, South Africa.
Amazon Web Service:
Launched Africa (Cape Town) Region in 2020 [7].
Microsoft Azure:
Launched South Africa datacenter in Cape Town and Johannesburg in 2019 [8].
It was actually quite tricky to find a reliable VPS provider in Lagos and I just used Google search to find any available one randomly.
Cloudflare Outages
Cloudflare experienced a serious outage, again [9]. Luckily, it only affects the control plane and analytics. They are always transparent in post mortem report.
[1] https://mathstodon.xyz/@tao/111206761117553482
[2] https://mathstodon.xyz/@tao/111360218854032278
[3] Lean 4 programming language and theorem prover
https://github.com/leanprover/lean4
[4] Learning Lean 4
https://leanprover-community.github.io/learn.html
[5] Scientific computing in Lean 4
https://github.com/lecopivo/SciLean
[6] New cloud regions coming to a country near you
https://cloud.google.com/blog/products/infrastructure/introducing-new-google-cloud-regions
[7] Regions and Availability Zones
https://aws.amazon.com/about-aws/global-infrastructure/regions_az/
[8] Microsoft opens first data centers in Africa with general availability of Microsoft Azure
Microsoft opens first datacenters in Africa with general availability of Microsoft Azure
[9] Post Mortem on Cloudflare Control Plane and Analytics Outage
https://blog.cloudflare.com/post-mortem-on-cloudflare-control-plane-and-analytics-outage/