• Nielius/Tensorlayouts A formal proof in Lean of when you can merge two tensor views (a shape/stride) into one. You could use that to improve performance in tinygrad/PyTorch: it tells you when you don’t need to copy the underlying data if you do certain operations on your tensor, such as transposing, slicing, reshaping, etc.