Jweb_Guru

Well, there is a more important sense in which solar is renewable but not tidal energy. The sun does not burn out appreciably more quickly if we use a larger percentage of the available solar energy, it's there whether we use it or not. This is not the case for tidal energy.

I will go further (since there are certainly bugs in the kernels of proof assistants, more frequently than you might imagine). Even if there is a bug in Lean's kernel, it will almost never invalidate a Lean proof, because bugs in the Lean kernel (or the kernels of other proof assistants) are, just like with normal programs, almost always bugs dealing with edge cases testing the boundaries of mathematics or syntax, not things that show up in everyday proofs. Coq has fixed numerous proofs of False and, to my knowledge, these fixes have never ended up invalidating a "real" proof that wasn't specifically designed to test these kinds of edge cases. Proofs are far more often broken by changes to the surface syntax (e.g. inference algorithms or the tactic language) than by changes to the kernel.

Obviously, this is not foolproof against malicious "adversarial" mathematicians, so knowing something was proved in Lean still requires some degree of checking. But it does make it pretty extraordinarily unlikely that a false proof in a proof assistant was arrived at by accident, which is far from the case with the "old" way of doing mathematics.

(I'd also add that the concern about getting the specification of a design wrong is something that rarely lasts longer than attempts to actually use it to prove anything nontrivial, since the proofs won't go through, but there at least can be a lot of debate about how to interpret specifications in some fields [e.g. computer science] or whether certain specs are "actually" equivalent to the statements someone wants to prove, especially for stuff like category theory where manual proofs have a good deal of handwaving... but these are minor technical issues compared to the viewpoint of the article).

Compilers are usually very reluctant to add "surprising" optimizations to atomics, even if they're fully justified by the standard, because (1) there are a lot of compiler bugs and/or holes in the standard that are only exposed after combining multiple optimizations involving atomics, (2) most programs explicitly use atomics only rarely, making it not the most productive thing to optimize, and (3) the programs and libraries that do use them are often reliant on them for synchronization, "liveness," or performance behavior that's not mandated by the standard. Common pathological examples include checks that assume the compiler won't skip assigning values if it can prove there's some obscure possible execution where the intermediate value can never be read, assuming that checking the result of a relaxed load in an if statement will guarantee that accesses run in the if will be sequenced after the read, etc.

A properly efficient sequence lock (no compare exchange or full acquire fence, relaxed loads for reads--which are less expensive on ARM than acquire loads, for good architectural reasons) isn't actually possible to write in C++ and I believe this was in fact a motivation for why Java atomics are the way they are. See https://www.hpl.hp.com/techreports/2012/HPL-2012-68.pdf. I suspect this is why Java added load-load.

We don't need a lot of things. A better example than plastic straws is beef: we definitely don't need beef, it's already expensive, and it has an extremely large and disproportionately heavy impact on CO2 consumption due to the combination of required grain, methane release, and needing land for cows incentivizing cutting down rainforest. Most people here would be pretty up in arms about any proposal to ban beef, so why focus on comparatively harmless stuff like lipstick and soda?

That's exactly where I'm coming from here. The original evidence that had people cautiously optimistic has been thoroughly dismantled. It's not showing any unusual or inexplicable signs of superconductivity: no anomalously high diamagnetism, no anomalously low resistivity or IV curves, no heat capacity differences, it lacks a theoretical model, and all anomalous measurements can be completely explained in terms of known or predicted properties of its constituent materials. I don't even need to bring up the lack of credibility of most of the members of the lab, HT Kim's crackpot tendencies, or the fact that Qcentre misrepresented its affiliations for it to be clear that there's nothing to the original paper.

Yet people are arguing "it might still be a superconductor! Just an exotic type that no one can replicate and also doesn't look like a superconductor in any measurements!" Okay, so could any number of other compounds, many of which are far more promising than this one (e.g. some USOs have shown actual definite diamagnetism). Why should we care about this one?

Iris photo is completely unconfirmed outside of "Twitter likes her." She said she would make a video over a week ago and never did. Additionally, due to the fleck being confined to a tube, it would not fall afoul of any proofs about ordinary ferromagnetic levitation being impossible.

That's not clear, but either way--as I've told you several times--there has been no credible demonstration of stationary levitation for even very weak uses of the word "credible."

I don't consider a replication attempt with a lab in a commercial relationship with another lab, that has essentially embargoed the results for six months, credible.

> Never claimed it was impossible, just that it's rare.

Okay, so? It's been experimentally verified and it's not some sort of novel behavior. It's even been predicted to occur in PbO before, just not observed until now.

> I don't care about reputability of anyone unless they have a known past of fraud. Gatekeeping in science is lame unless someone makes a claim to break well understood theory or claims to do something technically difficult. RTSC is neither.

RTSC is absolutely something we believe is likely to be difficult, but more importantly none of the replications by either verified labs or scientists willing to put their names on the line, who documented what they were doing, actually worked.

Meanwhile, we have videos like the one you linked, which are posted completely anonymously by someone affiliated with no institution who followed it up with two videos of spinning poop. Many people have demonstrated that it's quite easy to fake a video that looks like this using software like Aftereffects. For you to claim this video is equally trustworthy to replications by credible labs with reputations on the line is certainly a choice you can make! I will not be doing it with you, however.

It's not a room temperature ambient pressure superconductor. I should probably bet on it while there's still some value left here, I guess.

It's definitely difficult to synthesize reliably when people dismiss any replication attempt that doesn't show superconductivity as a priori not being the right compound.

> Ferromagnetic explains half levitation but it doesn't explain full levitation

No one reputable has actually demonstrated full levitation, including the original team.

> Sure, metal ones are, but Are ceramic ferromagnets (without iron) common? That lone electron in an orbital is pretty important.

They literally reproduced this behavior with a substance that looks identical to the original LK-99, so while it would be quite unusual, it is clearly possible. Apparently ferromagnetism without any ferromagnetic compounds has been witnessed before, e.g. in ZnO.

They were refusing to share them with anyone reputable until today. Today, they said they would share them, so hopefully this will all be over soon (but IMO it's already resolved).

There is, a combination of strong (but not amazingly strong) diamagnetism at low field strengths and soft ferromagnetism (in floating samples) at high field strengths. Which is exactly what the paper in the link observed while getting the same results everyone else has. The only unambiguous sign of superconductivity was the original resistance graph which can apparently be explained by contact issues with four point probes (you can argue that they must have done many experiments and surely didn't cherrypick just the one where they found "superconductivity", but consider the quality of the rest of the paper...)

People seem skeptical that it's actually been ruled out by that test. Regardless, that paper found diamagnetism on the level of pyrolytic graphite, which would be interesting in this material albeit not really evidence of superconductivity, but from what I've heard it is very easy to get anomalous reports of diamagnetism during zero field cooling if there is a high-temperature ferromagnetic transition, and you have to be extremely careful about your measurements and do lots of repeated tests to be sure. AFAIK, every other paper has either only seen very weak diamagnetism (expected given the compounds involved) or none at all.

It has been noted that graphite also exhibits "one-dimensional diamagnetism" (in the sense that it has much stronger diamagnetism in one plane than the other two) and it levitates fine and isn't very mysterious. There also haven't been any reliable measurements of strong diamagnetism in LK-99. We have the video from the team, which is not evidence of diamagnetism let alone strong diamagnetism, and we have a handful of magnetic susceptibility tests from labs on tiny, tiny samples (much smaller than the one in the video) that found weak diamagnetism.

I don't really think anything about LK-99 is optimistic at this point, honestly.

It's not necessary and they could simply offer it to other labs. The reason they have not done so (except to one small lab in South Korea that doesn't appear to specialize in superconductivity and claims they need six months to verify) is pretty obvious by now: they don't actually have a superconductor.

Yeah, it's good to see that because there were some concerning signs in the last day or so.

After reading some responses suggesting the authors don't understand how to measure superconductivity, I double checked the senior author's credentials. He is very much a legit scientist but seems to be a relative newcomer to superconducting. There is a long established history of respected and productive scientists entering fields they don't really know anything about and engaging in mild to moderate quackery. In this case, I am now fairly confident that the following is true:

* he and his team did discover a (probably) novel diamagnetic material. * it may or may not have interesting properties * however, it is not superconductive.

According to people who were able to more fully read the "real" paper, the key issue is that their measurements, if taken at face value (and not as due to, e.g., bad contacts with the material) suggest two contradictory things:

* the sample is extremely pure (due to the shape of the first graph).

* the sample has impurities causing it to not exhibit zero resistance, and not to exhibit "full" superconductive properties (i.e. having zero resistance under a magnetic field with increasing strength).

Additionally, since they were never able to measure Tc, they can't show the full Meissner effect as that requires heating up the sample to above its Tc first and then cooling it and flipping it, something you can't do with a diamagnet. By itself the fact that they didn't reach this temperature did not bother me, because I assumed that the senior authors were experts in superconductivity and had made sure that the material simultaneously exhibited other superconductive properties like zero resistance (or close enough when factoring in impurities). The fact that they were so focused on replication and the process was so simple made it unlikely to be fraud.

But, the fact that the first chart doesn't make sense unless the sample were completely pure, plus the lack of expertise they have with superconductors, indicates that it is much more likely measurement error on their parts, in which case it's not clear whether there's any evidence at all for superconductivity right now outside the diamagnetism. Given that there are many room temperature diamagnets known (albeit perhaps none as strong as this one?) and no room temperature superconductors known, this puts the odds that this isn't a superconductor at practically certain, IMO.

Not the same company, Quantum Energy Co vs Quantum Energy Research Center. Your article is from 2015 and features someone who is not involved in any of the papers or with the company.

I mean sure, it would not be hard to fake this if it's a total fraud. It will also be discovered almost instantly so I don't find that case interesting. The more interesting question to me is, (1) are there glaring red flags indicating it's a fraud (no), and (2) if it's not a fraud, what are the odds that it's superconductivity? For me, seeing how weak the criticism is, I'm moderately higher on it actually being superconductivity than I was before, since alternative explanations also seem to require materials with novel properties.

I will say this, I haven't found the "it's not real" responses very compelling either. I've also found that people who actually work in the field seem less skeptical than knowledgeable people adjacent to the field. If it's not fraud, it's at least something new. Here are the reasons I've seen provided by adjacent folks:

Nonscientific objections:

* it was published in a low h-index journal (not a scientific objection)

* poor formatting, misspelled title (not a scientific objection)

* patented and has a company (not a scientific objection)

* seems too simple, it has to be more complex than that, how could we have missed that? (not a scientific objection, also rather ahistorical)

I consider all of these pretty irrelevant given that the authors are not no-names and the actual paper makes clear claims, does exactly what everyone says you should be able to do if you have a real superconductor (show a video of it floating!) and makes replication easy. If it's straight up fraud it will be easy to discover.

There were also many pseudoscientific objections raised by field-adjacent people that I found uncompelling, responses from people actually in the field in parentheses:

* The first video looks like normal copper, the second like other diamagnetic materials or is otherwise unconvincing (not evidence against it being superconducting, at least one materials science lab had several members look at it and thought it looked legit).

* They are trying to hide the magnet structure somehow (the video shows it in clear view).

* The wafer isn't fully levitating or the way it falls is suspicious (not really unexpected given that the superconductive part is supposed to be present in only a few percent of the material).

Scientific objections I find more compelling made by people more familiar with the field, but more bourne of natural skepticism than disqualifying, with there being a lot of subtlety:

* both effects shown can be achieved in known ways by non-superconducting materials (but at the same time? would at least be a major material science advance in that case as it would apparently require diamagnetism ~ 150x as strong as graphite. Author who mentioned this said it would be "materials science magic" and I'm not sure why you'd rather believe in this than superconductivity given that neither have ever been seen before and it's consistent with sueprconductivty. Unless it's straight up fraud).

* Mesner effect graph don't go exactly to zero / happen exactly where you'd expect, maybe reflects a measurement error? (apparently, given the small % of the material that's supposed to be superconducting and material distribution, this isn't really evidence either way. not like we have other room temperature superconductors to compare it to).

* no max temperature where superconductivity vanishes measured, so is it really superconducting? (standard measurement devices only go up to what they reported, scientists seem very mixed about whether it would be easy to DIY measurement at higher temperatures for such a small current)

* not a similar mechanism to known good past "high-temperature" superconductors, and proposed explanation doesn't really make sense given slight deviations in pressure compared to what is in this substance (other scientists seem to disagree and think there could be something there, but it would also not be the first time something novel was discovered and worked for reasons totally different than those the scientists initially imagined)

Overall I find the quality of the objections really weak which increases (to me) the chances that there is something novel here, even if it's not superconductivity. That or it's obvious fraud and we'll know in like three days.

They're very much correlated, even though obviously they don't explain anywhere close to all of the obesity problem. A significant amount of food advertising is due to needing to find ways to sell the tremendous surplus of some crops, milk, etc. that the US produces due to these subsidies. Food advertising is known to be effective and is a contributor to obesity.

WASM's runtime is far simpler than JS's, or even something like the JVM, particularly due to lack of garbage collection. The language was deliberately designed to be straightforward and efficient to JIT compile to a safe virtual machine, e.g. attention was paid to making sure bounds checking could be elided efficiently for constant offsets while being enabled elsewhere. It's also significantly simplified compared to assembly, and lacks functionality like arbitrary jumps that are common sources of vulnerabilities. It's pretty much ideal for the usecase of "I want to run pretty fast code on an untrusted machine" which is the main reason it's taking off.

(Obviously, as WASM JIT compilers get more elaborate and it incorporates things like GC'd references, some of the advantages of this design wrt simplicity will disappear, but I anticipate that these kinds of features will mostly not be used in settings like databases).

I get what you're saying, I just think this is more of a Google thing than a TR thing. Their peer reviewed papers have the same issue as their preprints, TRs, and whitepapers, generally speaking--Google researchers feel no incentive to actually share how they did things, perform accurate or up-to-date comparisons to comparable frameworks, or even bother outlining their key contributions, because they know the paper will be published, widely read, widely cited, and influential even if they don't do any of those things. It's to the point that I think it might actually be house policy to neuter their papers of specific details as much as possible, presumably to retain what they perceive as Google's competitive advantage, because it makes no sense otherwise that wildly different papers with different authorship groups coming from so many different areas of CS could all have these same problems.

This is (IMO) quite different from, e.g., the cases of academics publishing misleading benchmarks, which is more often just being wedded to a bad idea because you spent years of work on it and your position is at risk if you didn't end up outperforming existing approaches. Often I can still get a lot out of papers with misleading benchmarks, even if what I get is "don't try this technique, it doesn't work." Whereas I frequently get nothing at all out of Google publications. If I had to describe the way Google seems to view academic publishing in one word, it would be "marketing"--it's advertising for people to either come work at Google or use their products, not something written with the intent of advancing the wider state of the art, or even the less noble goal justifying the time and money they put into whatever they're writing about.

I'm sorry, this is nonsense. Technical reports exist to fill in information that is useful for readers but not necessary to understand the key contributions of the work, and/or that don't fit within the journal or conference's page limit. I'm not sure where you got the idea that it is something people do to avoid competitive baselines; IME, the peer-reviewed portion of the publication is far more likely to contain misleading benchmarks than the technical report, since the paper is trying to "sell" the work in a way the technical report is not.

What this is an instance of is Google's approach to academic publishing of releasing a paper that contains almost no actionable information, but which is considered important and publishable solely because it came from Google and therefore is used in industry. This has been exhibited many times before--e.g. see the original Spanner paper, which was so light on details and confusing that they needed to release a followup paper several years later to explain what the system was even using the atomic clocks for!

If you believe you can find a memory unsafety vulnerability in this project's Rust code based on the existence of those bugs, feel free to do so.

That might well be the case, but it didn't translate to realtime play AFAIK.

Not really. The AI was essentially "cheating" to play inhuman micro, its macro was apparently just as bad as typically expected.