ducktective

Basically, LLMs have reduced the incentives in doing open source.

If you go with agentic route, randos with money to spare on latest models, beat you. If you go LLM-free, AI corpos say "all the better for us! More free untainted dataset!"

"air-gapped" how?

It's often suggested that Lean is a general programming language but I don't see typical libraries to do basic stuff in it, like an arg parser, web server, GUI, SQL integrations etc.

Can lean generate small static binaries the same way Go/Rust/C/C++ can?

How practical is rewriting, say, grep in Lean?

- Is it possible to train only on math and logic materials and expect the model's response in math questions to be superior to general models with the same training/inference compute hardware?

- Are there non-LLM approaches to the above task with the goal of achieving a non-hallucinatory agent?

A question to those active in chip design industry: Are formal methods and formally proving a design more prevalent and normal in this industry compared to general software development?

Like for a Arm microcontroller design, do engineers thoroughly test and formally prove the correct functionality of every component? If that's the case, why silicon errata is a thing?

>distillation datasets

You ask about distillation but I wonder, is there any training datasets (~ TB-order) available that startup folks in SV use or is it so that everyone has to create their own scraping pipeline ?

Don't worry, AI's gonna fix it in Rust in Windows 12

You're doing something serious aaand suddenly out of nowhere the fan starts screaming cause some cryptically named process decides right now is the time to get stuck in some loop

>outdated

What modern features are you looking for in a say, document editor? My experience with LibreOffice Writer and Calc has been excellent. I'm happy there is no modern AI or cloud integration noise or ribbon bars with excessive whitespaces.

For starters, universities and government offices should not expect a proprietary format. Everyone should accept OpenDocument Format (ODF) or a similar FOSS format. MS Office, LibreOffice, OpenOffice and whatnot can compete in editing and rendering open formats.

Come to think of it, this is a good proposal for EU, thanks for the USB-C, by the way :)

Tangential, but does anyone know why in 2026 and on Debian 13, my machine still hangs when some process exhausts RAM?

Is there really no higher-priority kernel process to prevent total freeze of the system and send a SIGKILL to the culprit process when such a scenario happens?

My point was, people block js of websites by default. Why? Cause website devs abuse js and don't exclusively use it for basic interactivity of stuff like sorting table columns.

There is an incentive to use HTML for common interactivity purposes.

>single, simple JS file

It's all fine and dandy until marketing bros decide to shove all kinds of shady modals into that JS file. The JS side is not exclusive to trivial interactivity.

> including isolated testing environments

Given the attack vector having possible super-human capability, I'm not sure such an environment exists. "Isolated" according to who?

Maybe seL4 could be a viable option here...

>Do you think Japan and the EU would be better off if our/their economies were centred around trillion dollar companies that make a product that is 20% better than the Chinese models at 1000x the cost?

Why Japan and Europe don't develop a model that is 20% worse at 0.001x the cost?

I wonder about Japan and Europe these days. Back in the 80s, when Japan was pursuing the "Fifth-Generation Computers", EU and US scrambled to compete with Japan. Like, it was a big deal for strategists and decision-making high-level politicians of that era.

Now in 2020s, it seems only China is tailing US and in turn, US is wary of China. What gives?

Do LLMs generate deterministic or trustworthy answers?

It's AI-assisted now but on a path to becoming AI-independent in the coming months at least due to the general public perception.

I wonder what experts think of this other option: going fully native for one platform then vibe-porting it to others.

No passion, no independent research, only the drive to make money with as little effort as possible

Exactly. I was wondering what language would be better for heavy agentic workflow. Due to a recent blog post, Clojure seem to be the most terse [1]. But some people are suggesting static types would help in this workflow.

[1] : https://martinalderson.com/posts/which-programming-languages...

Recent posts on formal proofs usually talk about Lean, Rocq, Isabelle and (due to this post) Metamath.

What do people think of F* [1]? At least, for non-mathematics projects, doesn't it seem to be a more appropriate option [2]? It seems even the CS community is gravitating towards Lean.

[1] https://fstar-lang.org/

[2] https://fstarlang.github.io/lowstar/html/Introduction.html

>that there's no daylight between the works of an individual who has taken a literal lifetime to hone a skillset and any random dilletante armed with the appropriate AI tools.

Well, the promise of AGI and current LLM trajectory looks like this is how it's going to be. This is part of the reason that juniors or university students feel animosity towards LLMs.

Have you looked at the recent prompts mathematicians use to disprove conjectures? One of the last ones related to graph theory was basically: continue research...enough partial results, give me a breakthrough...

Not exactly skillful prompting...

>a config switch between A and B is never considered

And why should modern corpo maintain additional complexity to pander to 1% of privacy-aware tech-savvy users?

>Still, one thing should not be forgotten, those who fail to adapt eventually fall behind.

Adapt to what? Current LLM endgame is "wished-spec => code". Where do you fit in this? You are fighting for the last 10%, 1%, 0.1% contribution in this march of the 9s game.

Thanks for the summary!

Does anyone happen to know how to make a Windows machine, the extended display of a Linux machine? Both machines are on the same network.

I'm looking to use a Windows laptop as a mere HDMI monitor for the Linux laptop. I don't need gaming/streaming requirements. Like, can anyone list our options in 2026 as the parent comment did?

I assume one can use this Moonshine on the server (Linux laptop) and run Moonlight on the client (windows laptop)?

Not even that, libssh2 vul. that "scp"s malware from cloud to your machine...

Before the advent of LLMs, ML was used in upscaling the assets and pre-rendered backgrounds of the first 3 classic Resident Evil games: https://www.reshdp.com

Makes one wonder, why should anyone embark on learning this intricate and time-consuming art of reverse engineering when LLMs are on their way to automate it in seconds...