boccaff

Probably it was his recent appearance on numberphile.

Any field where there is no external validator (formal proofs, compiler, rule sets) for AI to leverage and real world evaluation isn't easily digitalized. Add in a bit of physical interaction and it is done.

I don´t think so. For programming agents can run code, check compiler output, etc. For mathematics, it is almost the same once you factor in the usage of lean.

For the reality, you can´t close the loop that fast, or with that precision. You will have to slow down by several orders of magnitude.

I don't know, but I imagine "unsubscribe" type of features.

Don't we still need to verify that what the LLM proved is actually the stated system?If agents cutting corners (like deleting tests) is a concern, how can we be sure that the verification corresponds to the software and that every _load bearing_ assumption is true? I don't think that simply trusting the Lean core is enough.

The value of AI and related companies on retirement funds

There is a lot of "throw it against the wall, and if it sticks, write it up" empirical work against benchmarks. It leads to post-hoc rationalization of the work and browser plugins using LLMs to find references for work that is already written. It is a bureaucratic view about "you need a citation for this", where people misunderstand the citation as a checkbox, instead of "you need to substantiate this claim, as I, the reviewer, do not accept this as a fact".

The estimated area of no-till in Brazil is between 33 to 50 million hectares. It won't be hard for you to find videos of no-till corn being planted following soybean. There is also grass cover that is planted after the main crop season, that is later grazed. This cover stays till the next year and the new crop is planted without tilling. You may need to use "plantio direto" "milho safrinha" and "braquiária de cobertura" plus some translation.

llama models pushed the envelope for a while, and having them "open-weight" allowed a lot of tinkering. I would say that most of fine tuned evolved from work on top of llama models.

tree algorithms on sklearn use parallel arrays to represent the tree structure.

short answer: No.

longer answer: Random forests use the average of multiple trees that are trained in a way to reduce the correlation between trees (bagging with modified trees). Boosting trains sequentially, with each classifier working on the resulting residuals so far.

I am assuming that you meant boosted decision trees, sometimes gradient boosted decisions trees, as usually one have boosted decision trees. I think xgboost added boosted RF, and you can boost any supervised model, but it is not usual.

Do you have any pointer to search for that?