The only reason I think biotech companies are not yet raising hell (and invoking the False Claims Act) is that Thermo Fisher's antibodies are already known to be notoriously bad, and everyone serious seems to have to validate everything themselves.
I'd treat this about the same as datasheets for mechanical or electrical parts.
When I buy an electronic component as a regular consumer I expect the datasheet "typical" values to be accurate 90% of the time. I can imagine larger industrial customers would really raise a stink if it's worse than that. However, any critical components in my circuit must be verified and "binned", and that's on me.
This is the thing. Yes, the marketing material is bad. But, no one in lab trusts an antibody just because of where you bought it. A new antibody always gets tested and validated before use.
That is to say, this looks bad for Thermo Fisher. But, that’s as far as the damage should go.
Why would you even generate fake pictures of this type? Don't you already have real ones? I mean, it's actually more work, unless you don't have the real ones.
I’m not going to defend Fisher here. It was a stupid thing for someone to do.
But unless you’re in the field, you won’t realize exactly how big ThermoFisher actually is. They are the major supplier of everything for molecular biology work. From freezers (the Thermo part) to plates and pipettes (Fisher) to enzymes and antibodies. In many ways they are like Amazon. They sell everything. Some of it from outside companies, but a good deal of sales are from in-house brands. They could use their position as a reseller to know which products sell the best and with the highest margins.
In a company of this size, it’s easy to have one group feel pressure and cheat on running the gels to confirm results. Particularly when the real results are ambiguous or dodgy. It’s not a good look, but I doubt it will put a dent in people from buying things (non-antibodies) from them.
I was wondering the same thing, but near the end, the article discusses using statistical techniques to determine the standard error. In other words, you can easily get an idea of the accuracy of the result, which is harder with typical numerical integration techniques.
With many quadrature rules (e.g. trapezoidal rule, Simpson's rule) you have a very cheap error estimator obtained by comparing the results over n and 2n subdivision points.
Numerical integration methods suffer from the “curse of dimensionality”: they require exponentially more points in higher dimensions. Monte Carlo integration methods have an error that is independent of dimension, so they scale much better.
Typical numerical methods are faster and way cheaper for the same level of accuracy in 1D, but it's trivial to integrate over a surface, volume, hypervolume, etc. with Monte Carlo methods.
as i understand: numerical methods -> smooth out noise from sampling/floating point error/etc for methods that are analytically inspired that are computationally efficient where monte carlo -> computationally expensive brute force random sampling where you can improve accuracy by throwing more compute at the problem.
My understanding (which could be wildly wrong, I only skimmed the thread) is that it's running in a standard 2-dimensional Game of Life grid, it just happens to start out as a 1x3.7B cell line.
It's possible. It'd just be a 3D visualization and more importantly, stupendously huge. If each cell was a cubic millimeter, the shape would be 3700km wide, and stretch 1/3rd of the way to the moon.
And if each cell was a cubic micrometer (which is a side length 200-300 times smaller than a pixel on a typical screen and 50-100 times thinner than a human hair), it'd still stretch 3.7 kilometers, which is about the length of a commercial airport runway.
Be rest assured Ben’s previous job was in the medial imaging industry. While he worked on MRI machines rather than ionizing radiation, I think he’s very well aware of the dangers of X rays and has many projects dealing with ionizing radiation. There’s a lot of bad safety science YouTubers, Ben isn’t one of them :)
Funny thing: it’s actually rare to get radiation damage to human hands and feet since there’s not too much growing tissue there!
On the contrary, I was told stories in school that old IR doctors used to lose the hair on their hands after using the fluoro for years. The fingernails are also radiosensitive.
The main reason that X-rays of the hands and feet are usually very low risk is because the beam intensity (dose) required to penetrate the small amount of tissue is very low. Because the video uses a high-sensitivity detector (photon counter) the dose may be even less than usual. However, it would still be a regulatory violation if you did it in a hospital.
I’m not a mathematician, so could someone explain the difference in usage between Lean and Coq?
On a surface level my understanding is that both are computer augmented ways to formalize mathematics. Why use one over the other? Why was Lean developed when Coq already existed?
I think the difference is mostly cultural. The type theories of Lean and Rocq are fairly close, with the exception that Lean operates with definitional proof irrelevance as one of the default axioms. This causes Lean to lose subject reduction and decidability of definitinal equality as properties of the language.
Many people in the Rocq community see this as a no-go and some argue this will cause the system to be hard to use over the long run. In the Lean community, the interest in type theory is at a much lower level, and people see this as a practical tradeoff. They recognize the theoretical issues show up in practice, but so infrequently that having this axiom is worth it.
I consider this matter to be an open question.
If you look at what's being done in the communities, in Lean the focus is very much on and around mathlib. This means there's a fairly monolithic culture of mathematicians interested in formalizing, supplemented with some people interested in formal verification of software.
The Rocq community seems much more diverse in the sense that formalization effort is split over many projects, with different axioms assumed and different philosophies. This also holds for tooling and language features. It seems like any problem has at least two solutions lying around.
My personal take is that this diversity is nice for exploring options, it also causes the Rocq community to move slower due to technical debt of switching between solutions.
> The type theories of Lean and Rocq are fairly close, with the exception that Lean operates with definitional proof irrelevance as one of the default axioms. This causes Lean to lose subject reduction and decidability of definitinal equality as properties of the language.
Couldn't you introduce proof relevance as an explicit axiom into a Lean program to solve that particular issue?
Lean has a good library of formalized mathematics, but lacks code extraction (you cannot generate a program from the proofs it constructs). So it is more suitable and highly used by mathematicians to prove theorems.
Coq has always focused on proving program correctness, so it sees lots of use by computer scientists. It also does code extraction, so after you prove a program correct in Coq you can generate a fast version of that program without the proof overhead.
I think that (most) mathematicians were not that interested in formal proof until quite recently (as opposed to computer scientists), and most of the interest in lean has been self-reinforcing, namely there is a (relatively speaking) huge library of formally verified mathematics. So now basically anyone who cares about formal verification as a tool for mathematics is working in lean. There are of course numerous techincal differences which you can read about if you google coq vs lean.
Presumably they want to eventually put a human inside it, in which case having a humanoid robot to work off of wouldn't change the aero calculations and designs too much. The article talks about specific design considerations to avoid the exhaust gases.
Gravity Industries already has that sorted https://gravity.co/ . I was almost expecting this robot to just be a humanoid robot with one of those suits on
> Presumably they want to eventually put a human inside it [..]
I'm imagining a team just putting the organs of a human into the robot to save on space. Basically a brain plus whatever is absolutely necessary to run the brain.
Glad to see this! We need better treatments for OA short of a joint replacement.
I'm not too surprised that this treatment works. It's essentially like localized steroids to just the joint- killing off the immune cells causing inflammation.
Good features is that it's localized (so no systemic immunosuppression) and the risk of cancer is low since you rarely get radiation-induced cancer in joints because there's not enough dividing cells. Unfortunately heading to radiotherapy is a logistical challenge, but there are enough people suffering from OA that would happily do this to get relief.
> It's essentially like localized steroids to just the joint- killing off the immune cells causing inflammation.
Are you confusing osteoarthritis with rheumatoid arthritis? I didn't think the pain of osteoarthritis had anything to do with the immune response. You've literally got bone rubbing against bone. It's not going to feel good.
Both OA and RA involve some inflammation (-itis means inflammation). RA is more T cell driven inflammation (and clinically visible) while OA is more macrophage driven. Mechanical wearing still makes the joint unhappy at the cellular level- you just don’t see it big and red as a symptom like in RA.
reply