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.

Love this idea, although I wonder if this can also be done with QMK keyboards. I'll have to try setting up similar macros in my Ergodox EZ.

Interesting tips, but it also depends on the field.

If you're submitting to a control theory journal, you better have some novel theorems with rigorous mathematical proofs in that "rest of the paper" part. That's a little nontrivial.

> Because we always get back the same amount of numbers no matter how big or small the input text, we now have a way to mathematically compare any two pieces of arbitrary text to each other.

I think there needs to be some more clarification here. Hash functions also return the same sized output no matter how big or small the input text. However, mathematically comparing two hashes is going to have a much different meaning than mathematically comparing two embeddings.

I'd recommend emphasizing that embeddings are training dependent--the quality of comparison will depend on the quality and type of training used to produce the embedding. There isn't some single "universal embedding" that allows for meaningful comparison of arbitrary text.

> Rust is a subset of C++ with extra static checks

This is like saying that Julia is a subset of Python with JIT compilation. Rust and C++ have some conceptual similarities, but they are entirely different languages.

I'm seeing the same problem--the page crashes on mobile (Brave). On desktop it loads, but all of the code cells have a crashed page symbol in them.

Now all we need is a PDF reader embedded within a PDF. Bonus points for enabling it to open itself for infinite recursion.

Can confirm this. Teaching is a pass / fail grade for new professors to get tenure in most places. Your ability to get grant funding and publish highly cited papers are astronomically more important to the university than your teaching abilities.

I was told by a seminar speaker one time about a pre-tenure professor who was awarded his University's highest teaching award one day. The very next day he was denied tenure because he didn't publish enough.

I recommend reading the book "Tenure Hacks" [1] to anyone interested in pursuing a career as a tenured professor. I don't agree with all of the points in the book, but it is an important and eye-opening alternative perspective to the typical narrative surrounding academic positions.

[1]: https://www.amazon.com/Tenure-hacks-secrets-making-tenure/dp...