openquery

Thanks for sharing. I thought the discontinuous nature of the SNN made it non-differentiable and therefore unsuitable for SGD and backprop.

Excalidraw[0] and a mouse and a few failed attempts :)

[0] https://excalidraw.com/

Right. Ironically I chose a model that was around in the 1970s without knowing it.

My point was more a game-theoretic one. There is just no chance I would beat the frontier labs if I tried the same things with less compute and less people. (Of course there is almost 0 chance I would beat them at all.)

Give it a shot. It isn't much code.

If you want to look at more serious work the Spiking Neural Net community has made models which actually work and are power efficient.

Thank you for saying this. I agree which is why I wrote this up.

Hey thanks for bringing this up. I am the author. Could you please let me know which browser / OS you're using?

Also I'll be adding contact info soon, it's a new blog.

Looks like Dagger has a Rust SDK [0]! Going to give it a try.

[0] https://github.com/dagger/dagger/tree/main/sdk/rust

Uncle Petros and Goldbach's Conjecture.

A great, short read that gives you a very gentle introduction to the world of pure mathematics following the life of Uncle Petros, a mathematical prodigy who devoted his life to trying to solve Goldbach's Conjecture.

Ironically, this is one of the main reasons I didn't study mathematics.

> I foresee that lots of inference would be happening on local machines with models being downloaded on demand

Why? It's much more efficient to have centralized special purpose hardware to run enormous models and then ship the comparatively small result over the internet.

By analogy, you don't have a search engine running on your phone right?

This article is very well written and super informative. One thing I didn't understand is:

> At Answer.AI our north star is making useful AI more accessible. $150,000 to create your own high-quality personalized model definitely doesn’t count as accessible!

Renting an A100 on RunPod is ~$1.89 / hour. So you'd need ~80,000 A100 hours to train a useful AI model?

I agree completely. Ok, they hallucinate occasionally but so do humans.

Tireless, always online, no stupid questions interactive personal tutor for pennies.

> But at least in my case, whenever I tell people about some idea, I kind of tend to lose interest in the idea. So I just went to work on it instead.

I think that's great advice.

I rent spot instances on GCP with big GPUs on demand. It works quite well and since I'm just playing around I pay a very small amount per hour and kill it after I'm done.

This is the second piece of content I've ever seen using the same numbering system as Wittgenstein's Tractatus, the first of course being the Tractatus itself.

I'd love to see a demo video.

Winglang looks really cool. I'm really curious how Winglang will evolve their language syntax and semantics to make cloud development more expressive (I assumed `bring` and `inflight` keywords are just the beginning?).

At Shuttle[0] we've built something similar but instead of building a language from scratch we've built on Rust using metaprogramming and the type system to achieve the same effect. For now we haven't hit any limitations that would warrant a new compiler as metaprogramming allows us to express cloud development quite naturally inside the language.

[0] https://www.shuttle.rs/

What a giant of a man.

Thanks Charlie your wisdom and clear thinking. I hope I learnt something from your writings.

You will be missed.

Can automated theorem provers solve mathematical olympiad problems in a reasonable time given enough compute?

LLMs are quite good at generating semantically correct language. I remember reading a paper about extending the planning capabilities of GPT-4 by using a Planning Domain Definition Language [0]. By that same logic could an LLM not translate the olympiad problem into a form suitable for a theorem prover?

[0] https://arxiv.org/pdf/2305.11014.pdf

And here are the changes for the recently released v0.5: https://rocket.rs/v0.5/news/2023-11-17-version-0.5/

Proving a theorem given a set of axioms is a search problem. Given a set of axioms you can apply rules of inference to generate the graph of all provable theorems. Proving a theorem is about finding a path from the axioms to the vertex which is your theorem.

But you can make the same case for axioms - that they are not invented but discovered through a process of search in the space of axioms.

And the equivalent uom in Rust.

https://crates.io/crates/uom

The only video footage I've managed to find of John von Neumann.

Let's finish the quote.

> the intelligence & character of the masses are incomparably lower than the intelligence and character of the few who produce some thing valuable for the community.

It doesn't strike me as crazy that a guy who was hanging out with Gödel and von Neumann all day [0] might think this way.

[0] https://en.wikipedia.org/wiki/Albert_Einstein#Resident_schol...

If I had no contact with society from the 29th of November 2022 (the day before ChatGPT was released according to Wikipedia) and came back today to see the OpenAI keynote I would have lost my mind.

The progress and usefulness of these products is absolutely incredible.

> it seems that it has decided that because Rust is a good language for a platform (makes sense!) that it must be good for usage on the platform.

This isn't true - or at least it wasn't our thought process when starting to build Shuttle. Yes Rust made a ton of sense as the language with which to build the platform, but the point of Shuttle was always about providing a great developer experience to the end user. _That's_ why we chose Rust for the 'front end' of the platform.

Our position was that the amazing type system combined with generics, metaprogramming (macros) and excellent compiler errors would enable us to build something truly special when it comes to how devs build on Shuttle.

Congrats on the launch! Been waiting for this.

This argument can be made at any level of abstraction I think.

For example, you can make the same case for AWS Lambdas abstracting the infrastructure away from you, or VMs that run on-top of a hypervisor abstracting away the bare-metal servers.

IMO it really boils down to the quality of the implementation of a product and also designing your product such that if users need to debug (which hopefully isn't often) you offer that visibility into the internals.

Disclaimer: I'm one of the co-founders of Shuttle. Also, I haven't used Pulumi so I don't want to misrepresent it.

However, as far as I understand, Pulumi is an infrastructure _as_ code solution, offering an SDK in various languages which wrap providers enabling you to define your desired infrastructure. In the context of a cloud provider like GCP, this means wrapping the existing GCP primitives and services (i.e. GKE) and enabling you to declare your desired infrastructure in your favourite programming language.

Shuttle is an infrastructure _from_ code solution. The infrastructure that is provisioned for you is defined implicitly by your application's code. Static analysis is done at compile time to figure out what you need implicitly (i.e. if you're using a database connection pool, you probably need a database). Furthermore Shuttle offers its own primitives (i.e. secrets management) without a necessary correspondence to an underlying cloud provider (although there are some, like AWS RDS).

The nyan cat improvisation is even better imo.

I've been playing piano for a few years (no teacher, on and off) and have always been curious about the topic of sheet music. When you're first learning it's very painful. The notation isn't that bad, sharps, flats, time signatures etc - that part is ok. What _is_ difficult is corresponding a position on the staff to a physical note on a keyboard, especially when you have a treble clef and a base clef.

However over time it becomes easier and easier - and then you wonder is sheet music somehow optimal or is it 'good enough' and has withstood the test of time (also accounting for the fact that there is an enormous corpus of existing sheet music).

The question regarding this app (which looks awesome) is, is this format for reading music better than sheet music at the expert level (for professional musicians). And if not, how can we get that 10x improvement to make the switch from sheet music to something better.