Given its strength in mathematics, it seems likely that AI should be of great help with discovering new physics. We just need to teach it to ask interesting questions.
Dirac comments that he thinks a potential path to the discovery of new physics is to start with a mathematical domain and work outwards from there, guided by mathematical beauty. This is what I took OP's comment to be about - of course setting aside questions on an LLM's ability to recognize beauty
Superstring theory has been based on the idea of mathematical beauty, but it's run into serious complications when it comes to empirical results. Science is empirical first and foremost, because we need to verify that theories actually predict the universe we live in by testing them.
I don't know how LLMs would help sorting through the 10^500 possible universes when it comes to superstrings. You need to be able to run experiments or obtain observations.
Actually there are people attempting to find new math via biological entities. Cells and such. The interesting thing here is it is easily falsifiable even though working at these scales is still insanely hard.
Take the golden rule for example. It's a simple algorithm that shows up everywhere in nature. It represents the least amount of energy needed to assemble all kinds of structures. The gist here is nature finds these algorithms via evolution over billions of years and quadrillions of individual life experiments. We see life finding simple algorithms and platonic maths, how complex of algorithms has it found?
You no longer have to do an impossible number of experiments, instead you have to tease apart gene expressions to turn them on and off. Now, that is still a monumental task, but it's still doable in a reasonable amount of time.
Coronal mass traveling at a higher speed "sweeps" what's before it. You can see the spiral shape, and you can probably figure out that the stuff is slowing down as it moves outward.
Watch this occasionally for a few months and you'll get the idea, although solar activity is slowing down somewhat (as expected).
If you carefully re-read what GP wrote, you'll see there's no reference to Earth's orbit or 1 AU in there. GP wrote about the solar wind scattering cosmic rays when it reached some point in its outward travel.
I think so! You can codegen Ocaml directly, which means you have the benefit of lots of nice compiler libs and tools right out of the gate, but the metatheory is also expressive enough that your source language can be pretty wild with your denotational semantics. Grain of salt though, because I haven’t tried this concept in anger at all
personally i think you should just have a separate proof language that doesn't also try to be a programming language and build a bridge between them (ideally as a compilation target). anyways im working on this with my spare opus tokens.
What do you mean by this? I don’t want to be annoying and throw “propositions-as-types” at you, but as I understand it, F* is very much already doing this.
Its type system is the proof language/metatheory for making propositions, and its programs are their proofs, and there’s an intermediate form, core F*, that we elaborate to, a partial evaluation phase where we actually use the dependent types to simplify our AST, then codegen/lowering. In your analogy, I would call their core IR the bridge I guess? To clarify, I’m not trying to be a dick, I’m trying to sus out if I’ve understood you correctly
They started out that way. Keeping consistency between the formal specification and the code was always difficult. The further apart they are in distance or notation, the more difficult it is. So, the field experimented with verificatiom-oriented languages to localize changes.
reply