ubj

Good catch, link updated!

Dan Smalley's research lab at BYU is actively developing 3D volumetric holography technology.

https://youtu.be/N12i_FaHvOU

The video is a bit old, but it has a few fun demos of the capabilities they've developed.

This. Lean does not remove human responsibility, but it does assist in reducing the surface that the human needs to inspect and verify.

Now, there is also debate about what is lost when humans don't understand the proof body itself. It's a fair concern, and one we'll probably be wrestling with for some years.

> and/or have infants ricocheting around your home like screaming DVD logos

Slightly off topic, but as a parent I found this hilarious and will now be closely watching to see if any of my own screaming logos ever perfectly hit the corner of a room.

I've said this before, but it's interesting to see momentum go back and forth between the flexibility and ease of everyday language, and the formal rigor of programming languages.

It feels like we are still discovering the optimal operating range on a spectrum between these two domains. Perhaps the optimal range will depend on the specific field in question.

There was an interesting article in the Atlantic recently where a journalist spent a year participating in sports gambling. Part of the article discusses the effect it had on his psychology towards participants he had put his money on.

https://www.theatlantic.com/magazine/2026/04/online-sports-b...

Sports is one thing, but the potential for threats / intimidation towards news reporting, politics, etc. is a huge concern.

The author of the Airfoil article has made several similar tutorials on various topics:

https://ciechanow.ski/archives/

For machine learning, Distill.pub has some excellent hands-on tutorials. For example, here's one on momentum:

https://distill.pub/2017/momentum/

Octave has not implemented all of Matlab's functionality. You can see a list of Matlab functions that have not yet been implemented in Octave at the link below. It's a long list.

https://hg.savannah.gnu.org/hgweb/octave/file/tip/scripts/he...

EDIT: If the original link above isn't working, here's a fairly recent archived version:

https://web.archive.org/web/20250123192851/https://hg.savann...

Matlab is an great tool, if you can afford it.

It was a very unpleasant feeling when I graduated from my PhD and realized that most, if not all, of the Matlab scripts I had used for my research would now be useless to me unless I joined a company or national laboratory that paid for licenses with the specific toolboxes I had used.

I'm glad that a significant portion of tools in my current field are in open source languages such as Python and Julia. It widens access to other researchers who can then build upon it.

(And yes, I'm aware of Octave. It does not have the capabilities of Matlab in the areas that I worked in, and was not able to run all of my PhD scripts. I have not tried RunMat yet, but am looking forward to experimenting with it.)

This is apparently such a common misunderstanding that it was put at the bottom of the C++ iceberg:

https://victorpoughon.github.io/cppiceberg/

One of my students recently came to me with an interesting dilemma. His sister had written (without AI tools) an essay for another class, and her teacher told her that an "AI detection tool" had classified it as having been written by AI with "100% confidence". He was going to give her a zero on the assignment.

Putting aside the ludicrous confidence score, the student's question was: how could his sister convince the teacher she had actually written the essay herself? My only suggestion was for her to ask the teacher to sit down with her and have a 30-60 minute oral discussion on the essay so she could demonstrate she in fact knew the material. It's a dilemma that an increasing number of honest students will face, unfortunately.

Buzz Aldrin (who was the second person to walk on the moon) wrote his MIT thesis on methods for astronauts to handle the complexities of orbital dynamics when performing rendezvous maneuvers in orbit:

https://dspace.mit.edu/handle/1721.1/12652

Very curious to see what usage limits are like for paid plans. Anthropic was already experiencing issues with high-volume model usage for Pro and Max users. I hope their infrastructure is able to adequately support running these additional coding environments on top of model inference.

Just to be clear, I'm excited for the capability to use Claude Code entirely within the browser. However, I've heard reports of Max users experiencing throttled usage limits in recent months, and am concerned as to whether this will exacerbate that issue or not.

Platinum Medal: Complete a gold medal task in the presence of multiple children between the ages of 3 and 8. The children must remain safe throughout (and after) the entire process.

Science involves both deductive and inductive reasoning. I would in turn argue that mathematics is a science that focuses heavily (but not entirely) on deductive reasoning.

> Anyone knows what Mojo is doing that Julia cannot do?

First-class support for AoT compilation.

https://docs.modular.com/mojo/cli/build

Yes, Julia has a few options for making executables but they feel like an afterthought.

[EDIT]: I was wrong, uBlock Origin Lite was addressed by the article and does not have the same features.

I use Claude Max with it. Haven't personally tried the API yet.

I use DevPod [1] to run Claude Code within Docker-based dev container environments, and it's been fairly seamless. It lets me run environments locally and focus Claude's context on just the repo I want it to work on.

[1]: https://devpod.sh/

Where is Claude Code? Surprised to see it completely left out of this analysis.

This looks nice. I wasn't aware of Acorn--how much adoption does it have in the mathematics community (or formal methods / robotics / other communities)? I feel like most are rallying around Lean.

To me, the most exciting aspect of teaching mathematics using Lean is the immediate feedback. If a student's proof is wrong, it simply won't compile.

Previously, the only feedback students could receive would be from another human such as a TA, instructor, or other knowledgeable expert. Now they can receive rapid feedback from the Lean compiler.

In the future I hope there is an option for more instructive feedback from Lean's compiler in the spirit of how the Rust compiler offers suggestions to correct code. (This would probably require the use of dedicated LLMs though.)

Beautiful photos! I'd love to see a concert hall designed to look like something from this gallery.