Float is a tech startup founded by mathematicians with a bold vision: to build real-time vector embeddings that capture the instantaneous state of the world's financial markets. We aim to reflect every market, every supply chain, and every relevant piece of financial data. Our tech will combine cutting-edge AI/ML techniques with real-time processing of streaming data.
If you’re interested in training GPT models from scratch on a domain other than natural language, this is a great opportunity.
We're hiring for one role right now: Machine Learning Engineer
We're looking for experience with pytorch and an ability to reason about models mathematically. Experience with c++ is a plus.
Please email us (hiring at float dot trading) and mention HN in the subject.
Thanks! At the moment, we're focusing on the ML role, but please feel free to send an email explaining your background and interests. We can keep that in mind as we grow.
Float is a tech startup founded by mathematicians with a bold vision: to build real-time vector embeddings that capture the instantaneous state of the world's financial markets. We aim to reflect every market, every supply chain, and every relevant piece of financial data. Our tech will combine cutting-edge AI/ML techniques with real-time processing of streaming data.
If you’re interested in training GPT models from scratch on a domain other than natural language, this is a great opportunity.
Roles: Data Scientist, Software Developer, Machine Learning Engineer
Please email us (hiring at float dot trading) and mention HN in the subject.
I came here to see if this book made the list. I read it the summer before taking AP Physics. It made that class a breeze. Still, I'm impressed it made this list given it's not a CS book.
There are theoretical and potentially practical implications for this work. Black hole stability can be considered a kind of stress-test for General Relativity as a theory. If we believe the universe has rotating black holes, then we expect a valid theory to predict they are stable (or at least not catastrophically unstable). So a stability result helps validate the theory by at least showing there's one fewer way to refute it.
Some parts of the proof may actually be more insightful or practical than the result itself, but they don't get discovered or understood in detail until someone sits down and attempts to prove the result. If I had to guess, the most likely truly practical implication might be that some of the insights within the proof could help with numerical simulations of black holes. And if they help with numerical simulations of black holes, they might also help with numerical simulations of other PDEs that are more relevant in engineering.
I see a number of people commenting on the size of the proof (roughly 900 pages) which is not uncommon in this particular sub-field of PDEs. For context, I had the distinct privilege of studying under Sergiu Klainerman for my PhD on this topic. My own dissertation was about 600 pages. From my personal experience, I have come to understand a few factors that contribute to large proof sizes.
1. A lot of work is on inequalities involving integrals with many terms. These are difficult to express without taking up substantial space on the page. Some inequality derivations themselves might take multiple pages if you want to go step-by-step to illustrate how they are done.
2. Writing a proof of this size is not unlike building a medium-to-large size codebase. You have a lot of Theorems/Classes that need to fit together, and by employing some form of separation of concerns you can end up with something quite large and complex.
3. Verifying this kind of proof isn't usually done all at once. A lot of verification happens on the individual lemmas before they're pieced together. Once the entire paper is written, verification is more of a process where you rely on intuition for what the "hard parts" of the proof are and drilling down on those. But when writing the paper, you must of course account for all the details regardless of whether they are "easy" or "hard", and there can be many.
Having said all this, I have not read their paper and it has been 5 years since I was in this space. This is a truly remarkable accomplishment and the result of decades of hard work!
I'll end with an amusing anecdote. A fellow grad student, when deciding between U of Chicago and Princeton for his PhD program was pitched by a U of Chicago professor who once said something like "Of course you could go to Princeton and write 700 page papers that nobody reads." When this story was shared during a conversation over tea at Princeton, another professor retorted, "Or you could have gone to U Chicago to work with him and write 70 page papers that nobody reads!"
If these proofs really are like codebases, wouldn't we eventually expect these proofs to be written as software?
You'd install lemmas using a package manager and then import them into your proof.
You can then install updates to proofs. Maybe someone has found the proof to be wrong, in which case you either find a different proof or invalidate the lemma so all the dependents can be invalidated automatically.
That is not too far from what proof assistants actually do.
Agda is a dependently typed language (strongly resembling Haskell in Syntax, but with a lot more Unicode) where you rarely, if ever, "run" your programs but rather just check if they "compile", i.e. type check. If it does type check, you proved what you set out to prove.
And the individual lemmas could have author and chronology metadata attached, then you could plot the DAG as a roadmap/tech tree of sorts with an axis corresponding to time.
You'd be able to at a glance see the year a result entered public domain, who authored it, etc
I have wondered this as well. In theory, I want to say yes. But in practice, at least in this subfield, there are so many unimportant details that might make this really difficult.
It's not a perfect analogy, but some parts of the proof feel more like neural networks than procedural algorithms. So instead of verifying the composition of two procedural algorithms g(f(x)), you have something more like g(nn(f(x))), where nn is some sort of ML model / neural network. Interestingly, we are starting to see progress in importing ML models as libraries (eg Huggingface), so maybe that can carry over someday? I don't know.
Another challenge is simply a practical one. You would need someone heavily interested in both black hole mathematics and formal proof verification to be able to do this. Both of these require years of training.
Can anyone build on results that are so hard-won and complex that understanding them is as much effort as learning the basics of some entire fields of study?
Yes. That's how basically all expansion to the field of human knowledge is constructed today.
A human can only ingest and understand so much information in so much time. As Matt Might[1] eloquently described in "The Illustrated Guide to a PhD" [2], learning the basics of an entire field of study is what a bachelor's degree is for, a master's degree gives you a specialty, graduate students reading research papers like this one is how you get to the edge of human knowledge...only then can you start building on that sum of knowledge.
To summarize, a PhD often (maybe even typically) does not bring someone to the edge of human knowledge. Often a PhD gets people near it, but given the shear amount of scientific literature out there, it's difficult to know where the edge is.
I believe more than a few scientific PhDs do as well, and more than a few can become journal articles, or amount to a compilation of previously successfully accepted journal articles.
This item, an outstanding PhD thesis of an outstanding historian.
Free Soil, Free Labor, Free Men: The Ideology of the Republican Party before the Civil War
Some graduate students will likely spend a substantial part of their PhD understanding this paper. They will learn a lot in the process, and then they can contribute by either extending the result or finding a way to simplify a part of the proof. Or if they have a (very) related interest, they may be able to adapt some of the techniques to the problem they're interested in. Slowly over time, through this process, the knowledge might diffuse to other less related areas.
What an insane effort. And to think the peers of these folks that had to edit/accept this stuff had to check and verify the new math they came up with for the proof.
That’s my one issue — is it dubious we have to come up with new math to prove stuff? Or is that readable especially when dealing with such exotic things like black holes?
Would it be possible to create a proof of a proof?
Like : Given this list of assumptions -- This list of conclusions is proven to be true.
Maybe even with a confidence rating.
Then you could package your proof inside the proofproof. Thus sparing us the effort of reading it, and maybe even make your proof more widely appreciated.
In principle you could provide what's called a Probabilistically Checkable Proof. This would be a long string of bits, and a verifier would only have to sample 3 random bits to check the validity of the whole thing.
In practice we don't even make "normal" machine checkable proofs. They are just too much work. Maybe in the future when the machines are better at understanding us.
It probably wouldn't be too surprising if at least one error was lurking somewhere in those 900 pages. But if such an error were found, the authors would almost certainly be able to address/patch it very quickly. They have very good intuition for the "hard" parts of the problem and focus so much on those parts that it would be highly unlikely to overlook a critical error.
In particular,
1. You provide UI widgets (generated from your JSON schema, I presume) to generate the YAML and preview the result so the user can start building without having to invest so much time in learning your schema.
2. You represent web components in a structure (YAML/JSON) that is easy to manipulate with code.
3. Your project is open source so others can build on top of it. I'm amazed how almost every no/low-code project I have seen so far has some form of lock-in with expensive monthly rates when you finally want to deploy.
I recently started building something similar and was actually hacking on it past midnight last night only to wake up and see your post on HN (haha). But fortunately I haven't invested too much time in it--I'm going to rethink my hobby project and perhaps work on something that incorporates what you've done.
Thanks a lot. We were really excited the day we realised we could use Lowdefy to build our own docs, and that we could create a playground where you can see what happens when you change a property.
It would be very interesting to see what your ideas and approaches to the same problem are.
I definitely agree that this kind of tool is complex to build. We have our own model, which I have developed over a few earlier iterations of what we have available now, and we use it to draw all the objects to the canvas.
Generally speaking, there are two types of changes that we deal with. There are the changes that are very important, which don't happen very often, and then there are changes that are not very important but happen quickly. For example, when a user drags an object, each movement of the mouse is of the second type, while the final release is of the first type.
We make a distinction between what a user sees and the underlying "document" that a user is editing. When a user moves an object, we don't update the document until the user releases the move. However, we do send data to other devices so that anyone who is watching still sees the object being moved.
The video calling feature is based on WebRTC. (We also use WebRTC for streaming the data--so you can see other people draw in real-time, with Socket.IO as a fallback.)
Thanks for letting us know! At first glance, it seems to be an issue related to Heroku. We just tested the request invitation feature and it is working again.
Hi everyone, I’m John from Scratchwork (scratchworktool.com). This is a project I started as a math PhD student, because I was frustrated by how difficult it is to share ideas (mainly equations and diagrams) with other people on a computer. I designed Scratchwork to make it easy to draw complicated ideas by hand. For example, you can use your webcam to scan your drawings from a sheet of paper and they will be extracted and added as digital objects on the virtual board. These drawings can then individually be selected and moved around, deleted, etc. We’re also working on tablet apps, starting with the Samsung Galaxy Tab A with S pen, a relatively affordable tablet with an inductive stylus. As with basically all whiteboard apps, multiple people can work at the same time and see each others’ changes in real time. There is support for embedded video calls, which is admittedly somewhat buggy at the moment.
As the demo video illustrates, we have plans to support recognition of math expressions, allowing you to calculate by simply selecting some of your drawings and then applying operations such as simplify, differentiate, integrate, etc. The current implementation is not available publicly yet, and this is not our highest priority at the moment, but the eventual goal is to make it very easy to do calculations without needing to type equations.
This project is still a work in progress, but I would love to hear your thoughts and suggestions. Definitely sign up for our beta program. Also, please be aware that we are not permanently storing data yet, and many features are only partially implemented. Finally, we’re looking to expand our development team, so if you like this project and are looking for something new to work on, contact us at contact@scratchworktool.com.
This is definitely something we hope to do. Since we're still getting started, it's a matter of prioritization (not if, but when). We would love to hear more from you about your needs and that could help us expedite the feature. Could you please email us at contact@scratchworktool.com?
Along similar lines, we've been trying to plan an API for developers to use with our product. I'd love to hear if anyone has ideas.
Hey John, this is neat! Speaking to grad students at Columbia in both the math and physics department, I could see something like this really solving a problem. What led to you making this/what makes it different from every other whiteboard app on the web?
Thanks! I started making this after I bought a Macbook Air to replace my old Lenovo tablet PC. I really missed being able to draw precisely on a computer (which was possible with the tablet PC) and standard mouse input just doesn't do it for me.
Compared to other whiteboard apps, we're really focusing on alternatives to drawing with a mouse. My favorite feature (and possibly our most distinguishing feature) is the webcam scanner. It makes it really easy to scan a sheet of scratchwork and then rearrange terms and delete mistakes on the computer. Plus, it doesn't take a long time to draw the expressions, because you can do that with just pen and paper.
Float is a tech startup founded by mathematicians with a bold vision: to build real-time vector embeddings that capture the instantaneous state of the world's financial markets. We aim to reflect every market, every supply chain, and every relevant piece of financial data. Our tech will combine cutting-edge AI/ML techniques with real-time processing of streaming data.
If you’re interested in training GPT models from scratch on a domain other than natural language, this is a great opportunity.
We're hiring for one role right now: Machine Learning Engineer
We're looking for experience with pytorch and an ability to reason about models mathematically. Experience with c++ is a plus.
Please email us (hiring at float dot trading) and mention HN in the subject.