mauricioc

9 ms·

31.
by mauricioc 3y ago
https://en.wikipedia.org/wiki/Frequency_illusion perhaps?
32.
by mauricioc 3y ago
> He had a brilliant Yorkshire accent There's a talk of his on YouTube for anyone curious: https://www.youtube.com/watch?v=E8BNIohtyMQ (it's unrelated to Ramsey theory but also very interesting).
33.
Formalising modern research mathematics in real time(xenaproject.wordpress.com)
111 points by mauricioc 3y ago|16 comments
34.
by mauricioc 3y ago
It's a great book and I'm happy to see it get attention, but this was previously posted at https://news.ycombinator.com/item?id=38106860
35.
by mauricioc 3y ago
To emphasize chpatrick's point below, there are two definitions of "reproducibility" in this context: * Input reproducibility, meaning "perfect cache invalidation for inputs". Nix and Guix do this perfectly by desig
36.
by mauricioc 3y ago
Shumway happened before Flash EOL, so it's likely that Adobe forced development to stop. Although Ruffle existed before January 2021, it flew under the radar back then. Even if Adobe had no hand in it, it's much easier (and less r
37.
by mauricioc 3y ago
XP stands for "cross platform": https://www-archive.mozilla.org/xpfe/
38.
by mauricioc 3y ago
None of these proofs listed in the Wikipedia page are formalized in Lean at the moment, although a few are formalized in other theorem provers (Four Color Theorem in Coq, Kepler Conjecture in Isabelle). The "Formalization papers using
39.
by mauricioc 3y ago
Whoever wrote this was probably trying to showcase more of the language's functional features (or just trying to be clever). This works: def main := for i in [1:101] do if i % 15 == 0 then IO.println "FizzBu
40.
by mauricioc 3y ago
Mathlib was fully ported to Lean 4 ( https://github.com/leanprover-community/mathlib4 ), and the Lean 3 version is deprecated now. Edit: Adding a little bit more detail, it was ported one file at a time, using the automa
41.
by mauricioc 4y ago
For the example you cited (anonymous struct literals), there are two parts to it: 1) It omits the constructor name. My uneducated guess is that "modern" languages try to avoid the Java-style pattern of repeating a type/constr
42.
by mauricioc 4y ago
To whom?
43.
A Graduate Course in Applied Cryptography (2023-01-14 update)(toc.cryptobook.us)
2 points by mauricioc 4y ago|0 comments
44.
by mauricioc 4y ago
This is not an equivalent rephrasing. Although I make some pragmatic compromises every now and then, I think the GNU mission is important, and historically Linux has been an important part of the GNU system. GCC's copyleft license is a
45.
by mauricioc 4y ago
Thanks for the clarification! I didn't mean to say the two definitions were equivalent, as indeed they aren't. Rephrasing my second point to (hopefully) eliminate the ambiguity: There are two non-equivalent popular definitions for
46.
by mauricioc 4y ago
log(log(m))/log(m) tends to zero as m tends to infinity, which is what it means to be o(1). It is decreasing for m > e^e. Besides n^(1+o(1)), the other common definition for "almost linear" is precisely O(n log^k (n)) for
47.
by mauricioc 4y ago
Yes. (log n)/(n^epsilon) tends to zero for any positive epsilon, and so log n = n^(o(1)). The same holds for (log n)^k.
48.
by mauricioc 5y ago
The quoted sentence is an informal description of "positive density", and you can find the definition of density at https://en.wikipedia.org/wiki/Natural_density , or you can take a look at the first page of t
49.
by mauricioc 5y ago
Assuming you're talking about Bluetooth mics: If you're using pipewire-media-session (for example, if you're on NixOS 21.11 instead of NixOS unstable), then profile autoswitching [0] is disabled by default, so you have to use
50.
by mauricioc 5y ago
Firefox Reality also supports Servo as a browser engine, so this might be even more exciting! https://github.com/MozillaReality/FirefoxReality#experimenta...
51.
by mauricioc 5y ago
It's worth pointing out that Bowtell and Keevash proved a similarly impressive result for the toroidal case: https://arxiv.org/abs/2109.08083
52.
by mauricioc 5y ago
You say "practical values of n", but the answer to n = 27 is already known and I would be very surprised if the final result had any practical application. The point of these problems is rarely the numerical answer, but the develo
53.
by mauricioc 5y ago
I understood it as "(standard placebo) rate", not "standard (placebo rate)". That is: "standard placebo" (tablets) << "new placebo format" (injection with no active components) < "real d
54.
by mauricioc 5y ago
There's a very long interview with Kahan on ACM's YouTube channel. Here's a link to the part where he talks about the "Solve" button: https://youtu.be/smrs6FfnCzs?t=8670
55.
by mauricioc 5y ago
> So I looked at the version of Chrome on my parent’s computer. Version 76! I knew we were at ninety-something in 2022, so I figured that was the culprit. “I’ll just update Chrome,” I thought. > Turns out, you can’t. From what I could
56.
by mauricioc 5y ago
Nix will also be in Debian Bullseye: https://packages.debian.org/bullseye/nix-setup-systemd
57.
by mauricioc 5y ago
I am using GNOME 40 and I just opened a file picker in Totem, the official video player. I did not find a way to switch the file picker from "Details" mode (one line per file, with size/type columns and a very very small thum
58.
by mauricioc 6y ago
The Firefox mobile rewrite (Fenix) is just fantastic, and for me it is a huge improvement over the previous version. Many thanks to Emily and the whole team that shipped it, it's much appreciated :)
59.
by mauricioc 6y ago
Since type erasure was mentioned, it's worth noting that Philip Wadler (of Haskell fame) was involved both in the design of Java generics [0] and of Go generics [1]. (Perhaps I should clarify that I don't have a strong opinion on
60.
by mauricioc 6y ago
Unlike WhatsApp, the desktop app receives messages when the phone is off. Also unlike WhatsApp, messages received on the phone before you paired the desktop app do not get transferred to the computer.

More ›