kmill

24 ms·

181.
by kmill 5y ago
There's also a fallacy people fall into where they believe something doesn't affect them because they're not paying attention to it. People can be very unintentionally manipulative when they think they're just not being
182.
by kmill 5y ago
Hmm, I'm tempted to use it for mathscr... It probably would even be more legible.
183.
by kmill 5y ago
I believe you're explaining what a computable function is. A decidable set S of a type T is defined to be one for which there is a computable function f : T -> Bool such that the set of values x with f x = true is equal to S. A se
184.
by kmill 5y ago
It seems to me that id id id ... id always has type a -> a. If you're referring to the type of the first id in the sequence, then what you're saying makes sense.
185.
by kmill 5y ago
There was an interesting controversy surrounding the Algol-60 report. It seems many members of the committee wanted to be able to create implementations of the language that used only static allocations for activation records, but in the &
186.
by kmill 5y ago
A much nicer version of this is the Common Lisp condition system. Roughly the way it works is that in addition to being able to raise exceptions, a procedure can ask a condition handler how to proceed. Basically, the condition handlers ar
187.
by kmill 5y ago
omega = Y id where id = λx. x (though Y Y does not normalize either, infinite looping like omega)
188.
by kmill 5y ago
How are the ergonomics of a proof assistant based on λP2? Lean does a lot of elaboration of metavariables and typeclass instances and such before handing things off for checking by the kernel -- I'm curious about whether λP2's un
189.
by kmill 5y ago
Here's the definition of a subgroup in Lean's mathlib: https://leanprover-community.github.io/mathlib_docs/group_th... Given a group G, there is a type `subgroup G` of subgroups of G, and a subgroup is a stru
190.
by kmill 5y ago
And in "Lean style", refl proofs are a bit distasteful from a software engineering point of view because they pierce through the API of a mathematical object. (In the language of OOP, it can break encapsulation.) It tends to be a
191.
by kmill 5y ago
Given the definitions in a textbook on smooth manifolds, I agree with you -- the modern notion of a vector space has no notion of root or anchor since these words have no associated definitions. It's interesting to think about how we c
192.
by kmill 5y ago
Generalizing this, in the theory of differentiable manifolds, a vector (well, a "tangent vector") can be thought of as being an arrow rooted at a specific point. In Euclidean space (affine spaces), you can always translate all ve
193.
by kmill 6y ago
Yes, it's a theorem proving system, and it's based on foundations that are powerful enough to represent all of (formal) math. Including something like Lean excludes math itself from being able to do "specific concrete comput
194.
by kmill 6y ago
> If you mean it can, with appropriate software, do symbolic manipulations of general formulas that are valid for real numbers, yes, of course. But that's not the same as doing specific concrete computations with them. No, I don&#x2
195.
by kmill 6y ago
My computer can manipulate and prove things about real numbers just fine. I think it can do at least everything I can do normally, though much more laboriously. What I was mostly responding to in your previous comment is the idea of "
196.
by kmill 6y ago
Maybe I've been doing too much computer-assisted proofs recently, but I'm not understanding what all the fuss is. At some point you need a `Nat.mul` that's concretely defined, and probably the only reasonable definition is r
197.
by kmill 6y ago
I think it's sort of an illusion (though certainly a useful one) that numbers are all part of the same system. Multiplication of natural numbers is defined to be repeated addition, and I'm not really sure how you could define nat
198.
by kmill 6y ago
I think it would have to play well with Taylor series -- for example e^s would be 1 + s + s^2/2 + s^3/6 + s^4/24 + ... -- and that would be mixing units. That's not to say it's meaningless, but rather you'd ha
199.
by kmill 6y ago
I know we've discussed on HN before whether the elegance of the negative fragment extends to practice, but something about Lean is that it doesn't have LEM as an axiom. It's a theorem following from (a version of) the axiom
200.
by kmill 6y ago
A way to think about whether something is constructive is that everything is decidable, in the sense that there is some procedure that will give you the answer in finite time. In Kevin's example where you have two programs, one which d
201.
by kmill 6y ago
After working with Lean for a while, I've started to appreciate that there is a wider range of what it means to be constructive -- being "fully constructive" seems to me to be like fanatical efforts to make everything X, for
202.
by kmill 6y ago
I suppose it's not exactly mainstream, but Kronheimer and Mrowka are among those trying to prove the four color theorem using instanton homology and gauge theory. It's certainly not finite graph theory, though (their idea of a 3-
203.
by kmill 6y ago
I ended up writing one in the meantime -- check out the end of the readme. For this workload it seems to be a factor of 30x. The C program gets away with no heap allocation and inlining the entire render loop, though Lean does do quite a
204.
by kmill 6y ago
As I understand it, it does some static analysis still. The big idea with the Perseus algorithm, I think, is that instead of lending a reference at a function call, it is given . This leads to numerous optimizations where memory can static
205.
by kmill 6y ago
Yes to all. In Lean 3, they found it was great being able to write tactics in Lean itself, which has led to many nice tactics in mathlib. Lean 4 consolidates many lessons learned, and most of Lean itself is written in Lean now. In principle
206.
by kmill 6y ago
I did this to see how it was as a practical functional programming language, and I find I like the syntax and typeclass system more than Haskell's. One neat feature is that do notation had mut variables and for loops that get compiled
207.
by kmill 6y ago
Correcting my non-expert inaccuracies in this thread: I just learned that Diaconescu's theorem depends on the axiom of choice, which I'd missed even though I'd glanced at the code for classical.em a few times. So, LEM defini
208.
by kmill 6y ago
> it's useful to have a marker To whom? (That is rhetorical. The point is that this is not useful information for most mathematicians -- if you picked up a random graduate textbook in, say, algebra or combinatorics, I am certain th
209.
by kmill 6y ago
Right, that's what I am getting at. If it is as good as automatic, why make a mathematician do the transformation themselves? Why make them look at and manipulate all the transformed statements when they're working out a tactic p
210.
by kmill 6y ago
Ergonomics to me means "what is the moment-to-moment experience of a user of the language, in particular frictions between what the user wants to say and how it must be said." For someone who does not care much about constructibi

More ›