A formally verified Lean proof of the sensitivity conjecture, on Github: https://github.com/leanprover-community/mathlib/blob/3f216bc6a2c3729391ca1c8aaaf156fc96e7f10e/archive/sensitivity.lean#L389-L390 … More readable than I guessed (admittedly, a low bar), and very striking to see a significant result given a short formal proof.https://twitter.com/XenaProject/status/1260276915652485120 …
-
Show this thread
-
As an outsider, it's been exciting to watch the progress of these kinds of systems. I was very skeptical of them for a long time. But I was probably mostly wrong, or didn't appreciate their value.
1 reply 0 retweets 4 likesShow this thread -
Can't resist adding an orthogonal direction that I think has been underexplored: formal systems to support the heuristic thinking people use in creative problem solving.
4 replies 0 retweets 13 likesShow this thread
Solar-Lezama et al. advocated for sketch-based program synthesis as a means of algorithm discovery, e.g. to invent Karatsuba's multiplication method. ("Combinatorial Sketching for Finite Programs", ASPLOS'06)pic.twitter.com/bbr7ntA9iC
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.
cognitive psychology. PhD