HackerTrans
トップ新着トレンドコメント過去質問紹介求人

baruchel

no profile record

投稿

The million-dollar math problem hardly anyone is trying to solve

scientificamerican.com
2 ポイント·投稿者 baruchel·2 か月前·2 コメント

What Do Gödel's Incompleteness Theorems Mean?

quantamagazine.org
163 ポイント·投稿者 baruchel·2 か月前·65 コメント

The mathematician who doesn't exist

newscientist.com
3 ポイント·投稿者 baruchel·2 か月前·0 コメント

From Probable to Provable: What Automated Reasoning Means for the Board

mariothomas.com
1 ポイント·投稿者 baruchel·2 か月前·0 コメント

Mikan: a proof assistant for cubical type theory (forked from Agda)

mathstodon.xyz
2 ポイント·投稿者 baruchel·2 か月前·0 コメント

Why Not Use Lean?

lawrencecpaulson.github.io
6 ポイント·投稿者 baruchel·3 か月前·0 コメント

Rocq 9.2.0 Released

rocq-prover.org
2 ポイント·投稿者 baruchel·3 か月前·1 コメント

Eniac, the First General-Purpose Digital Computer, Turns 80

spectrum.ieee.org
127 ポイント·投稿者 baruchel·4 か月前·53 コメント

Can the Most Abstract Math Make the World a Better Place?

quantamagazine.org
5 ポイント·投稿者 baruchel·4 か月前·0 コメント

How many steps in a "chain of victories" separate you from your favorite player?

mastodon.online
2 ポイント·投稿者 baruchel·4 か月前·0 コメント

Assigning Open Problems in Class

blog.computationalcomplexity.org
18 ポイント·投稿者 baruchel·5 か月前·5 コメント

Mathematicians find largest prime number to date

fediscience.org
1 ポイント·投稿者 baruchel·5 か月前·2 コメント

Any chess position with 8 pieces on board and one pair of pawns has been solved

mastodon.online
18 ポイント·投稿者 baruchel·5 か月前·2 コメント

The Year in Mathematics

quantamagazine.org
3 ポイント·投稿者 baruchel·7 か月前·0 コメント

Ramanujan's 100-year-old pi formula is still revealing the Universe

sciencedaily.com
3 ポイント·投稿者 baruchel·7 か月前·0 コメント

The Year in Computer Science

quantamagazine.org
3 ポイント·投稿者 baruchel·7 か月前·0 コメント

Apples

xkcd.com
2 ポイント·投稿者 baruchel·7 か月前·0 コメント

50 years of proof assistants

lawrencecpaulson.github.io
144 ポイント·投稿者 baruchel·7 か月前·30 コメント

New Font Release: Bhs

fsd.it
1 ポイント·投稿者 baruchel·7 か月前·0 コメント

The Little Theorems

blog.computationalcomplexity.org
1 ポイント·投稿者 baruchel·8 か月前·0 コメント

コメント

baruchel
·13 日前·議論
https://zippythepinhead.com/Merchant2/merchant.mv?Screen=PRO...
baruchel
·4 か月前·議論
I can confirm the TT-RSS app (found on F-Droid) is very good. I have used it for years. On the other hand, the web app is not very good, and each time I wanted to read articles on my computer from the web interface, I encountered huge issues (for some reason, the "right click / mark as read" never correctly worked on my computers, or at least with huge lags of several seconds). When my free TT-RSS provider closed, I decided to switch to FreshRSS and could compare several apps for Android; I finally set up the following workflow: free FreshRSS account + "Read You" (found on F-Droid also), and managed to achieve a very similar workflow than previously (with a much better web app).
baruchel
·4 か月前·議論
Yes, but don't forget his formal work also (Hoare logic).
baruchel
·4 か月前·議論
If I remember correctly, this picture is commented in the very good book "Exact thinking in demented times", together with Mach's ideas.
baruchel
·6 か月前·議論
I’ve practiced array languages extensively myself, including for code golfing, and I fully understand the intellectual joy they can provide. But as I’ve gotten older, I’ve come to see a deep mismatch between what these languages present as “elegant” and what I find truly elegant from a computer science perspective.

Sure, realizing that the foobar of x is nothing more than the transpose of the 15th foo of x, combined via an inner product with the 7th bar of x raised to the power of baz, can be an ineffable intellectual delight. But actually computing that, rather than writing a “boring” loop, feels horrible to me. To my eyes, a “boring” piece of code written by Dijkstra in some Algol-like language contains more beauty than all these dazzling sleights of hand that hide zillions of loops under the rug while pretending that the actual computation doesn’t matter.
baruchel
·7 か月前·議論
When you compute some nice and elegant result, dissipated heat is an undesired side effect. But let's face it: we are speaking about proof of work. Proof of work means that a computed has run during some "required" time. In other words, you have to prove that enough heat has been dissipated. Waste of energy actually is "by design" here.
baruchel
·7 か月前·議論
Exact thinking in demented times by Karl Sigmund
baruchel
·8 か月前·議論
> Typography nerds are some of my favourite nerds.

A very detailed summary for another font (by the creator of the font), including ancient materials as well: https://mass-driver.com/article/md-nichrome-on-spacing-and-s...
baruchel
·8 か月前·議論
I don’t want to argue about the overall trend based on a single example, but Terence Tao’s substantial use of Mastodon for communication does change the picture a bit.
baruchel
·8 か月前·議論
As some readers may not be familiar with the name Xavier Leroy, I just want to emphasize that he is one of the people behind OCaml and a leading figure promoting Rocq/Coq.
baruchel
·8 か月前·議論
Shameless plug: eight years ago, I created the following website for posting plots of complex functions using similar gradients: https://kettenreihen.wordpress.com/
baruchel
·8 か月前·議論
I wrote the main application for my wife's business — she's a psychologist. That was only a few years ago, but as a senior lecturer in the more theoretical parts of computer science, I never really needed fancy UIs with flashy graphical effects. So I built a core engine and used the classic dialog tool as the thin user-facing layer.

At first, my wife was pretty disappointed — as a computer science teacher, wasn't I supposed to know how to build a “real” app? But a few years later, she doesn't want anything else. I even offered to have one of my students create a nicer UI without changing the engine or database, but by now she's completely used to the terminal menus.

The tool keeps a database, collects data through dialog forms, generates PDF invoices with groff, and launches Thunderbird when needed (to send invoices, etc.).
baruchel
·8 か月前·議論
Which is why functional programmers believe in the separation of Church and state. https://wiki.c2.com/?SeparationOfChurchAndState
baruchel
·9 か月前·議論
> It really is mind bending how fast this function grows.

While the BB function is obviously a well-defined function over the integers, I find it helpful to think of it as a function over qualitatively heterogeneous items—such as stones, bread toasters, mechanical watches, and computers. The key idea is to view the underlying computing devices not as “a little more powerful” than the previous ones, but as fundamentally different kinds of entities.
baruchel
·9 か月前·議論
May I suggest the Greenchess website? https://greenchess.net/ It certainly has some huge potential: nice minimalist interface and probably about 50 or 60 chess variants for all tastes. Some of them are obviously more or less "recent". You can easily start a new game or accept a pending invitation. I would call the set of players quite "active" and certainly motivated. But it is true that the pool of players remains small and you generally play against the same players again and again.
baruchel
·9 か月前·議論
Without paywall: https://www.removepaywall.com/search?url=https://www.scienti...