Show newer
Gavin Zhao boosted
Gavin Zhao boosted
Gavin Zhao boosted

#ScientificAmerican recently reprinted an interview I had a few months ago on the future of proof assistants and #AI in #math: scientificamerican.com/article . In it, I made the following assertion:

"I think in the future, instead of typing up our proofs, we would explain them to some #GPT. And the GPT will try to formalize it in #Lean as you go along. If everything checks out, the GPT will [essentially] say, “Here’s your paper in #LaTeXmath; here’s your Lean proof. If you like, I can press this button and submit it to a journal for you.” It could be a wonderful assistant in the future."

This statement seems to have received a mixed reception, in particular it has been interpreted as an assertion that mathematicians would be become lazier and sloppier with writing proofs. I think the best way to illustrate what I mean by this assertion is by a worked example, which is already within the capability of current technology. At terrytao.wordpress.com/2016/10 I have a moderately tricky problem in complex analysis. In chatgpt.com/share/63c5774a-d58 , I explained this problem and its solution to #ChatGPT in an interactive fashion, and after the proof was explained, GPT was able to provide a LaTeX file of the solution, which one can find at terrytao.wordpress.com/wp-cont . GPT performed quite well in my opinion, fleshing out my sketched argument into quite a coherent and reasonably rigorous full proof. This is not 100% of what I envisioned in the article - in particular the rigorous Lean translation in order to guarantee correctness is missing, which I think is an essential requirement before this workflow can be used for research quality publications - but hopefully will illustrate what I had in mind with the quote.

Gavin Zhao boosted
Gavin Zhao boosted

First full day running @buddiesofbudgie #Budgie Desktop on top of a Wayland compositor. Even in it's still very heavily WIP form.

Panel exclusion zone now implemented and thanks to some rubber ducking / help from @EbonJaeger , figured out what was wrong with my Budgie PopoverRedux.

Old Budgie.Popover code is gone, all the popovers are using the new implementation which are basically just Gtk.Popover. It'll be renamed back to Budgie.Popover once I do cleanup of PopoverManager and maybe refactor some more code.

Screenshot shows the bluetooth applet... well now being shown, as well as VS Code not being allowed to be maximized under the panel.

Biggest usability thing next for me will be making Raven not 100% full screen and the panel to always be set to the primary monitor rather than whichever monitor is in focus.

Gavin Zhao boosted

In math research papers (particularly the "good" ones) one often observes a negative correlation between the conceptual difficulty of a component of an argument, and its technical difficulty: the parts that are conceptually routine or straightforward may take many pages of technical computation, whereas the parts that are conceptually interesting (and novel) are actually relatively brief, once all the more routine auxiliary steps (e.g., treatment of various lower order error terms) are stripped away.

I theorize that this is an instance of Berkson's paradox. I found the enclosed graphic from brilliant.org/wiki/berksons-pa to be a good illustration of this paradox. In this (oversimplified) example, a negative correlation is seen between SAT scores and GPA in students admitted to a typical university, even though a positive correlation exists in the broader population, because students with too low of a combined SAT and GPA will get rejected from the university, whilst students with too high a score would typically go to a more prestigious school.

Similarly, mathematicians tend to write their best papers where the combined conceptual and technical difficulty of the steps of the argument is close to the upper bound of what they can handle. So steps that are both conceptually and technically easy don't occupy much space in the paper, whereas steps that are both conceptually and technically hard would not have been discovered by the mathematician in the first place. This creates the aforementioned negative correlation.

Often the key to reading a lengthy paper is to first filter out all the technically complicated steps and identify the (often much shorter) conceptual core.

@mashiro 站长,小森林(网页版)有这个功能吗?没找到 :pio_cry:


QT: [metalhead.club/@thomas/1125137]
Tom Tailor :damnified:  

I'd like to remind all Mastodon users that you can add a language filter to any follow relationship on Mastodon.

If you follow me and you don't speak German, you can easily remove my German posts from your timeline by adjusting the language settings.

Go to my profile page, select the dot menu and click "Change subscribed languages". Then select the languages that you speak.

This really is a hidden gem 💎 on Mastodon and not many people seem to know this feature :awesome:

#mastodon

Gavin Zhao boosted

I hope this email finds you well, and taking better care of yourself.

Gavin Zhao boosted
Gavin Zhao boosted

At last, some information from Google that students can really use!

Gavin Zhao boosted

this might be the first haskell program in the world that natively runs on arm64 windows

Gavin Zhao boosted

user: hello company, i would like to access your main product, you know, the one people come to you for, the main thing

company: HAVE YOU HEARD OF A I

Gavin Zhao boosted

During lunch a friend mentioned that you can just supply a HTTP URL to vim on the command line and it would use curl to download that resource and allow you to edit the content. I jokingly asked whether if you enter :w it would then issue a HTTP POST back to the origin which is of course ridiculous.

It issues a PUT

Gavin Zhao boosted
Gavin Zhao boosted
Gavin Zhao boosted
Gavin Zhao boosted
Gavin Zhao boosted
Gavin Zhao boosted
Gavin Zhao boosted

[Well-Typed Blog] Improvements to the ghc-debug terminal interface

`ghc-debug` is a debugging tool for performing precise heap analysis of Haskell programs (check out [our previous post introducing it](well-typed.com/blog/2021/01/fr)). While working on [Eras Profiling](well-typed.com/blog/2024/01/gh), we took the opportunity to... #haskell

well-typed.com/blog/2024/04/gh

Show older
小森林

每个人都有属于自己的一片森林,也许我们从来不曾走过,但它一直在那里,总会在那里。迷失的人迷失了,相逢的人会再相逢。愿这里,成为属于你的小森林。