HN user
In my experience, lean will show that it's correct, but does it not lose the mathematical intuition that led to the result? As far as my experience goes, that's really hard to encode in lean itself.
Could we maybe get more information about the problem from the LLM trace itself here?
Is it this one? https://github.com/landstrip/landstrip
Lean also has https://www.leanexplore.com and https://loogle.lean-lang.org/
If by dead-weight you mean the two speed Europe, I don't think that's possible. That weight is what makes the EU such a large market.
Surprisingly, it's the whisper model itself that does that. I find that it's also good with false starts, often correcting something like: "uhm, we could...we can go there" to just "we can go there", if spoken rapidly enough.
If anyone wants to try this without the intricate setup, if you have a linux system, you most probably can just press Ctrl+Alt+F3 and drop into a tty console directly. To return, you have to press Ctrl+Alt+F1 or Ctrl+Alt+F2. You also have multiple consoles, up until F12 probably.
I used to use this a lot when trying for a less distracting desktop, just like in the original post.
Doesn't llama.cpp (or similar) have to evict the kv cache for this, so that performance is degraded when running multiple sessions? Or how do you load a model in memory and then use it in multiple sessions? I am still learning this stuff
How do you use `pi` to ssh? I use `oh-my-pi`, and tried the `/ssh` command, but I couldn't get it to work. Then I saw a suggestion somewhere to just run `!ssh` to place things into the agent's context.
Is there a way to use it like "The current directory is at `ssh server`" and have the agent work from there?
I am very out of the loop. What is wrong with TP Link? What are the risks with it?
This is about the newly release Qwen3.6. Just wanted to make sure you got that correctly.
Has anybody figured some of the best flags to compile llama.cpp for rocm? I'm using the framework desktop and the Vulkan backend, because it was easier to compile out of the box, but I feel there's large peformance gains on the table by swtiching to rocm. Not sure if installing with brew on ubuntu would be easier.
Or add your real name to photos of you stored in Google Photos.
If by the spirit, you only mean the bazaar model, then yes. But it's in the original spirit of free software. GNU preferred to keep the development somewhat contained, even so many years ago.
It's sticky on the web though:
This is really nice to know. I remember trying to compile pandoc to Wasm after finding out that ghc had Wasm support, hitting all kinds of problems and then realising that there was no real way to post an issue to Haskell's gitlab repo without being pre-approved.
I guess now with LLMs, this makes more sense than ever, but it was a frustrating experience.
Some were already that and even more, because of other reasons. The Cathedral model, described in "The Cathedral and the Bazaar".
I found Geoffrey Hinton's hypothesis of LLMs interesting in this regard. They have to compress the world knowledge into a few billion parameters, much denser than the human brain, so they have to be very good at analogies, in order to obtain that compression.
This is explained in more detail in the book "Human Being: reclaim 12 vital skills we’re losing to technology", which I think I found on HN a few months ago.
The first chapter goes into human navigation and it gives this exact suggestion, locking the North up, as a way to regain some of the lost navigational skills.
Didn't see the website at first. Thank you!
This seems really nice, and looks like something I have been wanting to exist for some time. I will definitely play with it when I have some time.
I know this is a personal project and you maybe didn't want to make it public, but I think the README.md would be better suited with a section about the actual product. I clicked on it wanting to learn more, but with no time to test it for now.
That sounds awesome. But I have two curiosities: What are the problems of httpx? And was pycurl not enough for what you wanted to do?
I have been looking for the same thing, either from Meta's SAM 3[1] model, either from things like the OP.
There has been some research specifically in this area with what appears to be classic ML models [2], but it's unclear to me if it can generalize to dances it has not been trained on.
For small edits, has anybody configured a leader-key scheme? Something like Doom Emacs has with space as a leader.
It seems to me to be the best possible configuration for Emacs on Android (on a phone) and I was wondering if I should invest time in such a solution.
strokes-mode.el would also be very nice, but apparently it doesn't have touchscreen support.
As soon as I found out that this model launched, I tried giving it a problem that I have been trying to code in Lean4 (showing that quicksort preserves multiplicity). All the other frontier models I tried failed.
I used the pro version and it started out well (as they all did), but it couldn't prove it. The interesting part is that it typoed the name of a tactic, spelling it "abjel" instead of "abel", even though it correctly named the concept. I didn't expect the model to make this kind of error, because they all seems so good at programming lately, and none of the other models did, although they did some other naming errors.
I am sure I can get it to solve the problem with good context engineering, but it's interesting to see how they struggle with lesser represented programming languages by themselves.
Made me think of this SMBC comic[1], where there's a debate if being in English or Spanish, each with around a billion speakers, makes it rare or not.
How do you solve the second mission (the man that is hiding somewhere)? I've managed to find even the three.js mention, but nothing to start that one.
I think those kind of glasses may be really useful for blind people. I have seen similar glasses targeted at blind people, that at least in theory, seemed to me like a good idea.
I recall the glasses also can write on the screen inside the lens, which makes me think they may be good for deaf people as well.
It's just that these use-cases seem uncool, and big companies seem to have to be cool in order to keep either their status or their profits. But I have a feeling the technology may be really useful for some really vulnerable people.
This is exactly the fine-tuning I am hoping for, or I would do if I had the skills. I tried it with gemma3 270M and vanilla it fails spectacularly.
Basically it would be the quickadd[1] event from google calendar, but calendar agnostic.
[1] https://developers.google.com/workspace/calendar/api/v3/refe...
How do you use the recordings as part of the CI?
How exactly does it take 20 minutes to get an invite? I have not tried it, but I can't see how that would be easy.