Atiscant

Just a second recommendation for this movie. It is very good. It encapsulates part of my favorite danish psalm which translated is something like “An average happy and productive life on earth”. There is some ambiguity in the message in the movie, and I do not think it recommend his life, but it a very interesting contrast to most peoples life

I mean, even if could produce generic metal would it produce Igorrr? Meshugga? Tim Henson? Baby Metal? All of these are driven by other things then just producing metal. I agree pure AI music would properly rejected unless there was some point to it. I could see it have some part, but then as a weird instrument. Take a model for music, randomly mutate internal weights and then let it produce a drum beat. Keep doing that unless you hit some limit and perhaps that is interesting.

It is kind of ironic that the AI building tool is so hostile to AI. Copilot studio really is a hot mess, at least for me.

My wife and I are very different people. She is intuitive, involved in people, in the moments. I am slow, considering, post-hoc. We converge on Pratchett. We both read all the books, and been through all audiobooks (both new anf old). It’s become shared metaphors and a common frame of reference. We both have have a tendency to return to one or another of the series once or twice a year. I would have loved more, but I am deeply grateful for what we got.

I had a similar experience explaining logic, especially nested expressions, with cats and boxes. Also for showing syntactic versus semantic. We _can_ use cats if we wanted and retain the semantics. Also my proudest moment as a teacher was students producing a meme based on some of the discrete mathematics on graphs. They understood the point well enough to make a joke of it.

(Same reply as to another comment in this thread)

In Denmark the official identification app does basically this. When you to officially verify yourself for e.g. the bank, government sites or whatever you type a “username” (identity string that officially should not be linkable to you but in practice often is). The site then displays a QR code that you scan with phone and then approve with a slider. It is not perfect but it is fairly easy for everybody.

In Denmark the official identification app does basically this. When you to officially verify yourself for e.g. the bank, government sites or whatever you type a “username” (identity string that officially should not be linkable to you but in practice often is). The site then displays a QR code that you scan with phone and then approve with a slider. It is not perfect but it is fairly easy for everybody.

Would you mind adding some details about how this is actually setup?

It is interesting enough, but the report kind of feels very AI generated and generic. Most of the questions present the choices in a good vs bad way, i.e it sounds bad saying I disagree and sounds good when I say I agree. Other test usually have postive versions of both ends of the spectrum which is missing here. I also agree that there needs to be some validation of why these dimensions, how the correlated internally etc.

As noted in another reply, the natural numbers example is contrived, but illustrative. Nevertheless, if you have a set theoretical foundation, e.g. ZF/C, at some point you need to define what you are doing in that foundation. Most mathematicians do not and happily ignore the problem. That works until it dont. The whole reason Vladimir Voevodsky started work on HoTT and univalent foundations was that he believed we in fact DO need to be able to pull definitions back to foundations and to verify mathematics all the way down.

Sure you can work around it most of the time, but some times you cant. The whole point is that isomorphic is not equality in set theory, and sometimes proofs does not transfer along isomorphism because they refer to implementations. I agree that it is much preferable to work with abstract structure, but that not always what happens in practice. The natural number example is contrived but easy to see. My point of view is also that I do not like the Lean approach. It would actually like no junk theorems to exist in my theory. I am much more partial to the univalent approach and in particular univalent implementation that compute e.g. cubical. Regarding how easy it is to formalize, you are right. Lots of good work happens with set theory based type theory. My point was also that set theoretic foundations themselves are very hard to formalize, e.g ZFC + logic is very difficult to work from. A pure type theoretical foundations is much easier to get of the ground from. To prove that plus commutes directly from ZFC is a nightmare.