Hadamard asserts that no mathematical discovery is purely logical. The unconscious mind ... played a crucial role in the development of rigorous mathematical arguments. This role, and the handoffs between the subconscious and conscious minds, were distilled by Hadamard into the following framework for mathematical discovery:
- Preparation (primarily conscious)
- Incubation (primarily unconscious)
- Illumination (primarily unconscious)
- Verification (primarily conscious)
DeepMind's AlphaProof is too "conscious", missing Incubation and Illumination, and hence does not work well. In contrast, LLMs are more "unconscious", emulating Incubation and Illumination better, and thus have better chances to make math discoveries, at the risk of producing false results.
However, LLMs that reason in languages are still not "unconscious" enough; the Looped Language Models (by ByteDance) can reason in an even more unconscious way, aligning better with Hadamard's observation that "in addition to being non-rigorous, unconscious thought is often not even interpretable ... all mathematicians think without language or precise symbols, and many do not even use clear images", leading to higher reasoning capabilities.
A combination of the two approaches (AlphaProof and LLM) seems to be able to close the loop of Preparation - Incubation - Illumination - Verification in math. In addition, this framework is promising in "any domain that can culminate in a Verification step", and LLM may do the unconscious "Incubation - Illumination" part in many domains in addition to math (e.g., physics), but the "Verification" part differs across domains.
Good point. My strategy is to buy a new laptop (Thinkpad X1 Carbon) every one or two years and install the latest LTS of Xubuntu, so that a 3-year support is long enough for me.
Over the years, I have developed my notes and scripts to configure quickly a newly installed Xubuntu system on a new computer, so that everything works in the same way as on my old computer. Since I stick with the same brand of laptop (Thinkpad X1 Carbon), I do not feel any difference after the configuration, except that the computer becomes more powerful. I do not want to spend my time on adapting myself to a new system or a new computer.
Buying a new laptop so frequently may sound a bit expensive. It is indeed not if you spend so much time on your laptop as me. A more powerful laptop means that I can finish my work (e.g., numerical experiments) in (much) less time. In this sense, my life is prolonged. This is the only case I know that a common person can effectively trade an affordable amount of money for a longer life, as I often tell my students.
Not really. But I have introduced (enforced ...) deepin [1] to my wife, who is definitely not a "computer person". She essentially uses only WPS, WeChat, and Chrome. She did complain a few times in the beginning, requesting me to "get her Windows back", but I resisted and the complaints somehow stopped after the first month. This may be a sign that the system is not toooo difficult to use, and that I am an extremely lucky man with an extraordinarily forgiving wife --- I do not advise you to try the same unless you are as lucky!
Ubuntu is my first and last Linux distribution, which I have used for 16 years without discontinuation, since my early PhD days up to today.
The only change during the 16 years is that I switched from Ubuntu (with Gnome) to Xubuntu (with Xfce) [1], but I still call it Ubuntu. When people ask me about the difference between the two, I respond "color". I spend 90% of my time on the terminal, and I prefer the gray-blue style of Xfce and its lightness when I use the window system during the other 10%.
Before starting Linux, I had a very limited idea about what a computer is and how it works. An anecdote I often relate to my students is that I once copied the icon of an application (Turbo C) from one computer to another, believing that I could use the application on the second computer. Linux has taught me what a computer really is.
An "achievement" may be worth mentioning: in the past 16 years, essentially all my work as an applied mathematician has been typed under terminal using Vim, including papers, lecture notes, slides, programs, and particularly my 200-page PhD thesis in Chinese. It was not quite trivial to type Chinese in Vim --- think about it: how to get a Chinese inputting system that can work seamlessly with Vim's key bindings? Fcitx would not work (at least it was the case 13 years ago).
https://zhangzk.net
http://libprima.net
http://github.com/libprima/prima