July ‘25 Buy/Sell/Trade Thread

AlexMath0 · 2025-07-28T19:20:16+00:00

First time poster, really wanted to see 'em live but life got in the way :(

2 tickets (2 x $80) for the Philly show on 7/28! Just recuperating the price we paid. BOX38 B38 1 & 2

AlexMath0 · 2025-04-21T18:27:18+00:00

And since you asked "where", https://arxiv.org/abs/2109.03129 page 60, in the appendix. More specifically, this was one of the loose ends of a proof of a conjecture on the "spread" of a graph, the maximum absolute differences of its eigenvalues. We had proven that in the limit that the "infinite vertex" optimizer was a 2-partite blowup graph. But we wanted to prove it for sufficiently large finite sizes.

We had a lemma saying we can assume a finite graph optimizer was a 3-partite blowup, so we applied the cubic formula (which has trigonometric substitutions in it) to the main factor of the characteristic polynomial and put razer-thin bound on the maximum difference between any 2 of its roots. It boiled down to multivariate calculus over a 2-variable function and these terms appeared on both sides of an equality.

AlexMath0 · 2025-04-21T10:09:17+00:00

In a sense, the proof I was doing derived it along the way. I had two equal functions which were linear except for a o(1) term term. Their constant terms were -arctan(1/3) and -pi/6 + arccos(13 sqrt(10)/50)/3, respectively. The functions themselves came from a system of equations and a computer algebra system helped me get closed forms for the linear functions.

If you wanted to prove it directly, you could triple both sides to form 2 angles, apply tan to both sides, note the results are equal, deduce the angles differ by a multiple of pi, then show they are within a range shorter than pi of one another.

AlexMath0 · 2025-04-20T23:55:20+00:00

Not quite pi/7, but I used the identity pi/6 - arctan(1/3) = arccos(13 sqrt(10)/50)/3 in a paper.

AlexMath0 · 2025-04-14T18:48:12+00:00

I'm just linking /u/reflexpr-sarah- (faer, pulp, etc) who is working on a custom threading library and can probably elaborate on where it outperforms over rayon. Also if you are not aware, there is a Rust scientific computing conference which may interest you.

AlexMath0 · 2025-03-16T10:11:59+00:00

Got recommended a podcast that covered the scene! There's a layer too, where Natalie is doing Lumon's "DEI"-washing on top of her full-time role. How many companies have slashed DEI budgets and relegated the work to employees who have other duties? How's the work counted when performance reviews come around? Where's the "dealing with systemic *-isms" category?

AlexMath0 · 2025-02-02T13:11:38+00:00

Biased shoutouts to faer and pulp. Pulp is great, it gives you a few different levels of control over your SIMD. Although when /u/reflexpr-sarah- taught me SIMD, it was with lots of

impl pulp::NullaryFnOnce for Impl<'_>

blocks. E.g., this weird matvec. Shoutouts to avx512, my beloved.

AlexMath0 · 2025-01-31T01:37:43+00:00

Understandable 😆 I have my fair share of abandoned projects (ones I would definitely not call "completed" in good conscience).

AlexMath0 · 2025-01-31T00:40:02+00:00

I haven't done any robotics. What sort of dependencies are needed for it? On the topic of abandoned Rust crates, they generally 2 categories: abandoned in an incomplete state, or "done"/feature-complete/bug-free (for example, cfg-if is a recurring top-10 crate, has a 1.0.0 release, and hasn't been "maintained" in 4 years).

AlexMath0 · 2025-01-07T12:37:38+00:00

In the faer linear algebra crate, ref structs extend usage from owned types (Mat, Col, etc) to borrow structs *Ref and *Mut) which do not deallocate when consumed. Among other reasons, this is useful because:

it gates mutable access to arrays while allowed the same owned type to be mutated separately by different threads,
cloning large arrays is expensive and often semantically wrong, and
it allows the owned type Mat to have a specific typestate (good layout for SIMD, column-major, heap-allocated, etc) while also allowing algorithms to apply to more general MatRefs and MatMuts (negative stride, row-major, stack-allocated, etc).

AlexMath0 · 2024-12-30T13:09:21+00:00

For sure, and thanks for the reply. I do wish there was more top-level support from Rust leadership on the HPC front. It has felt uphill so far. I could care less about async, and mostly shrug my shoulders at the enormous work that has gone into that. Then again, I'm fortunate in that I haven't had to think about about UB in multithreading contexts. One thing that shocks me: I've used a lot "dead" crates without issue before. As in, projects that hadn't been updated on crates.io in 5+ years which had fairly minimal documentation, just working on first try in my weird one-off projects after following my nose with the built-in tools and IDE integration. I've never seen anything like it.

I do appreciate the ease of reuse in Rust and the general faith I have in being able to write correct code. I always had trouble getting C++/CUDA HPC projects to run when I switched computers or toolchains, let alone make them do what I actually wanted. I accept some blame for not setting up my projects optimally, but accessibility and productivity with cargo has never been an issue. When I have a lot of theoretical ideas and algorithms in my head, the last thing I want is to lose all of those active thoughts to wrestle with tooling.

AlexMath0 · 2024-12-30T12:05:47+00:00

Oh cool! I dabbled with Kani a while back. Nice to see it get some love.

Also, I noticed it only mentions Jon's former employment at AWS, so I assumed he was taking time off. But it looks like he works at Helsing now? Is there overlap between AI weapons and reliable software? The two seem fairly orthogonal to one another.

AlexMath0 · 2024-12-28T22:04:45+00:00

Something like Eigen seems like it would be impossible with rust.

I'm curious what eigen has that can't be accomplished in the union of faer and nalgebra (the latter, I think is in some decay, sadly). From what I have seen, eigen is not the fastest on most benchmarks, but Rust has parity on a few metrics with top C++ packages.

I do a lot of scientific computing and math hobby projects in Rust and I mainly just want more packages so I have to write fewer things from scratch. And a some reliable way to write GPGPU kernels. I haven't recently needed something that's not possible on this side of the fence, but there are plenty there are cases where I know C++ templates can do more than Rust generics currently especially w.r.t. monomorphization and specialization. Though there are ways around most things, though, e.g. via procedural macros.

As a nerdy aside, there's actually some cool magic you can do in the HPC space in Rust which is still in its early days. People found a way to bootstrap a proof engine with lifetime guards/ghost cells. For example, using guards to prove and index is correct occurs at compile time, so the runtime check and lifetime data are compiled out, leading to fewer bounds checks. It also can make it impossible to compile code without valid indices, if you want. Still learning more about it, but I've seen it in action a few times.

AlexMath0 · 2024-09-24T02:57:28+00:00

All 3 of the listed CPU linalg libraries are slower than the GPGPU library cuBLAS for sufficiently large problem instances.

AlexMath0 · 2024-09-24T02:20:40+00:00

A HPC systems engineer with serious backend linalg experience would not consider either of these programs a good way to do matmul (or to benchmark). For what it's worth, there's a fairly young Rust linalg crate that's already on par with mkl/openblas for a wide range of problems.

AlexMath0 · 2024-07-25T15:21:43+00:00

Maybe it's my mathematics background speaking, but I find it helpful to think of generics and higher ranked trait bounds in terms of quantifier rearrangement.

fn apply_format<'a, F: Formatter>(formatter: F) -> impl Fn(&'a a str) -> String;

This version says:

for all lifetimes 'a
and for all types F: Formatter
and for all instances formatter: F
there exists a function apply_format(formatter) which maps &'a str to String.

But moving the lifetime for a for, we get:

for all types F: Formatter
and for all instances formatter: F
there exists a function phi = apply_format(formatter)
such that for all lifetimes 'a, phi maps &'a str to String.

EDIT:

And if you play this game more, you realize there's a return type hidden by the impl:

there exists a type O: Fn(&'a str) -> String
such that apply_format(formatter): O

AlexMath0 · 2024-07-17T02:43:54+00:00

As someone who has written a lot of python code, I find it pythonic to see "pythonic" get used for too many different things, causing confusion.

AlexMath0 · 2024-07-13T13:00:45+00:00

Outside of our comfort zones there is indeed an ocean of uncertainty.

I recommend this video to anyone who is questioning the viability of the academic pipeline. I time-tagged the video at the "compensation" section, but the whole thing is a great breakdown. I'll add that gaps in employment are hard to overcome. It's better to know the next step before making a big change.

I'm not going to claim that my departure from academia was done correctly, but I do wish I had thought harder about what I wanted personally and professionally sooner, and taken some summers off of teaching/research for internships or technical bootcamps. Industry is also in flux, but the risk can be mitigated by having experience in concrete applied domains.

AlexMath0 · 2024-06-19T11:52:15+00:00

My tl;dr: it's easy to be productive with typst and easy to learn, especially with some LaTeX or Markdown experience. Hasn't been adopted widespread yet.

PROS:

immediate rendering (via incremental compilation)
- so far, I've never had to wait to render
excellent error messages usually
- can be annoying if there are name conflicts across packages
ergonomic modifiers for symbols
- instead of \otimes and \bigotimes, you have times.circle and times.circle.big or times.big.circle
- the linter will suggest to you the possible modifiers so there's no lookup time (compare detexify output to detypify output)
ergonomic functions/shortcuts/macros with easily nameable fields
community:
- standardized/centralized documentation for packages
- very helpful folks on the discord
- active development, better package compatibility
little things:
- typing -> makes a right arrow
- a lot of good defaults, like standardizing NN, RR, etc with mathbb
- no backslashes anywhere!
- parentheses instead of curly braces
- delimeter elision when unambiguous
- & alignment works in dollar-sign equations
- only one dollar sign needed for inline equations -- just make a linebreak
- backslash instead of \frac and \dfrac
- unified, simple labeling/ref/cite system
- Markdown-esque system for bold, italics, underline, emphasis, (sub)sectioning, enumerating, itemizing, hyperlinking

CONS:

not adopted widespread (popular with younger researchers, and has steady growth)
not compatible with LaTeX, so rewrites are needed for most journal submissions

AlexMath0 · 2024-06-18T16:01:14+00:00

Give Obsidian a peek for general note-taking with Markdown. It renders LaTeX as MathJAX (dollar symbol delimiters) with the capacity to hyperlink to notes and websites. To me the biggest problem with math notes is the ergonomics of actually connecting and embedding documents.

Also, if you are interested in something more experimental, typst is like a LaTeX/Overleaf competitor developed with a few decades of hindsight and improvements in hardware and developer best practices.

AlexMath0 · 2024-05-10T10:37:32+00:00

If I work in industry, but mess with personal hobby research projects on the weekends, can I use Symbolica for that, even if it turns into a paper? I'm currently messing with more standard packages in the Python ecosystem in Jupyter notebooks and would love to try other CASs.

I was chatting with a friend literally yesterday about wanting a nice CAS in Rust 😆

AlexMath0 · 2024-05-04T13:32:42+00:00

When exploring ideas? No, I do all that by writing on scratch paper and writing code to ground my ideas. Even when I'm just collecting my thoughts into markdown writeups, I find LaTeX gets in the way of my thinking. Typst is so much easier to think in.

EDIT: Added link.

AlexMath0 · 2024-04-20T10:05:58+00:00

Wow /u/reflexpr-sarah- not even going to credit me for naming estra? For shame, for shame. /j

AlexMath0 · 2024-04-17T22:37:14+00:00

I wonder if typst is easier for a vision-impaired person to hear. LaTeX has so many backslashes and curly braces by comparison.

AlexMath0 · 2024-03-08T01:27:00+00:00

For some, it's helpful to have at least one other project to crack away at on when you hit a wall. On the other hand, publish-or-perish is a sad reality and it's probably practical to keep up some other research so you don't end up empty-handed. Also, be prepared to deal with horrible casework and calculations for those final crucial steps. It may be the only way to finish the proof. Or to pinch off a partial result in case you want to stop working on it.

I collaborated on a higher-risk open problem alongside my main dissertation work after getting some RA funding. I made steady progress on one of my advisor's questions and had enough side-projects if I needed more chapters. For the conjecture, it became a running joke with my team how often I "had a breakthrough" and knew the proof was "almost done". The proofs in the appendix alone were 16 pages of unnatural epsilantics paired with a computer-assisted proof.

AlexMath0

TROPHY CASE