Profile

Cover photo
Andrej Bauer
Works at University of Ljubljana
Attended United World College of the Adriatic
Lives in Ljubljana, Slovenia
761 followers
AboutPostsPhotosVideos

Stream

Andrej Bauer

Shared publicly  - 
12
2
Boris Borcic's profile photoKonstantin Solomatov's profile photo
Add a comment...

Andrej Bauer

Shared publicly  - 
 
The evil publishers are dying slowly but surely. Here is another nail in the coffin. The important thing is not the book itself, but the technology around it (it's a configurable textbook where you get to choose what to include and what notation it should use!) and the fact that it has been done at all.
 
We’ve kept this on the down-low long enough, I think: together with Aldo Antonelli, Jeremy Avigad, Nicole Wyatt, and Audrey Yap, I’ve been working on an open source advanced logic textbook for a little while; Andy Arana and Gillian Russell are also on the…
We've kept this on the down-low long enough, I think: together with Aldo Antonelli, Jeremy Avigad, Nicole Wyatt, and Audrey Yap, I've been working on an open source advanced logic textbook for a li...
View original post
20
4
Ross Duncan's profile photoAntoine Padva's profile photo
Add a comment...

Andrej Bauer

Shared publicly  - 
 
Suppose we have a triangular mesh in 3D. I would like to "flatten it out" onto a plane, assuming this is possible, for instance because I took a mesh of a torus and cut it along a longitude and a meridian. The mesh is "stretchy" in the sense that we need not preserve the distances between the nodes. What would be a good phisical model for accomplishing this? It does not have to work in all cases, only fairly reasonable ones.

Here's one attempt: put equal electric charges into the vertices of the mesh so that they repel each other, and make all the edges into springs obeying Hook's law (with some natural length). This is not good enough yet, I think.
2
Carlos Scheidegger's profile photoAndrej Bauer's profile photoDan Piponi's profile photo
7 comments
 
+Andrej Bauer You clearly aren't watching enough of the zombie genre. I feel bad for the people who need to compare their finite element modelling of crash test dummies with ground truth.
Add a comment...

Andrej Bauer

Shared publicly  - 
 
Educational math videos can be really helpful, but it takes too long to make them. I spent 3 hours on this one. It answers a question on the hott-cafe mailing list.

#homotopytypetheory
12
2
Bas Spitters's profile photoAndrej Bauer's profile photoJim Stuttard's profile photoDavid Roberts's profile photo
8 comments
 
Mathematica and Keynote, you know, those closed-source commercial apps.
Add a comment...

Andrej Bauer

Shared publicly  - 
 
How to make #LaTeX beamer slides with notes, and use #Skim-app to show the notes on your laptop during your talk: https://gist.github.com/andrejbauer/ac361549ac2186be0cdb
- Gist is a simple way to share snippets of text and code with others.
5
3
Bas Spitters's profile photoDavid Roberts's profile photoPeter Luschny's profile photoli kev's profile photo
3 comments
 
Thanks pdfpc seems useful.
Add a comment...

Andrej Bauer

Shared publicly  - 
 
I know about standard references for solving recursive domain equations. But how about recursive predomain equations? One way to deal with them is to take the category of predomains and partial continuous maps which are defined on an open subset, because that category is equivalent to the category of domains, so presumably "things work out". Is there a standard reference for this sort of thing? (It should treat locally continuous functors of mixed variance, preferably on ω-cpos.)

#domaintheory  
1
Add a comment...
Have him in circles
761 people
Dan Farmer's profile photo
khaled bhuyain's profile photo
Frederick Kintanar's profile photo
Gregor Cerinšek's profile photo
Michael Witbrock's profile photo
Peter Kuzma's profile photo
a bahari's profile photo
Noam Zeilberger's profile photo
Irma Walter's profile photo

Andrej Bauer

Shared publicly  - 
 
I got a letter (excerpt quoted below), and I wonder what the best reply would be. I usually reply, respectfully and to the point. I once found a bug in a two-page proof of Fermat's theorem by a person who wrote math competently but made an honest error involving gcd's. He couldn't get anyone to look at his proof. He thanked me for putting him out of his misery. The present case seems more difficult. Perhaps that video of Vi Hart would help? What do you usually do?

"Respected sir,
Here I am representing different method than others so please go through it. ....[stuff omitted].... The whole world assumes that pi is transcendental number but I want to prove that pi is not transcendental. If you keep this concept apart from your brain & read the whole proof you will also get that assurance. If pi is transcendental then 1 = 0.99999… which is not exact?
.... [stuff omitted] ....Thus I found that the value of π is (17 -8√3)."
1
1
Chris Seib's profile photoAndrej Bauer's profile photoAndrew Miloradovsky's profile photo
31 comments
 
Well, I do not appreciate such language. I am closing off this discussion because it is a complete waste of time.

Andrej Bauer

Shared publicly  - 
 
My student wrote a book on C++!
 
Our new book is out! Learn about the past, present and future of C++: https://www.jetbrains.com/cpp-today-oreilly/
1 comment on original post
7
Gašper Ažman's profile photoPhilip Thrift's profile photoUrs Schreiber's profile photoAndrej Bauer's profile photo
6 comments
 
Well, Gašper is one of those people who could write a fast program even if he had only clay tables and a toothpick. So I think when he says that C++ code is "readable" you need to understand that correctly. Urs is teasing, but as a teacher I am really proud of Gašper.
Add a comment...

Andrej Bauer

Shared publicly  - 
 
It's my pleasure to announce a second PhD position in Ljubljana. It will be surpervised by Alex Simpson, and is in the general area of programming languages and computational effects.
It is my pleasure to announce a second PhD position in Ljubljana! A position is available for a PhD student at the University of Ljubljana in the general research area of modelling and reasoning about computational effects. The precise topic is somewhat flexible, and will be decided in ...
9
1
Philip Thrift's profile photo
Add a comment...

Andrej Bauer

Shared publicly  - 
 
I am trying to understand why certain math problems are difficult for our freshmen. In the "Logic and sets" course we had the following question, which turns out to be difficult:

"Is there an uncountable family of uncountable subsets of the plane such that any two of them intersect in a countably infinite set?"

They did countable and uncountable sets in our course as well as in the analysis course. We did Cantor's theorem, they know that rationals are countable and reals uncountable, and the midterm had the following question: "Are there two uncountable subsets of the line which intersect in a countably infinite set?"

If anyone wants to perform experiments on their students, I'd love to hear the results.
2
Timothy Gowers's profile photoAndrej Bauer's profile photo
8 comments
 
As it turns out the problem was not so hard after all. About a quarter of the students solved it. The most common solution was to take a family of straight lines unioned with a fixed countable set (such as the natural numbers as a subset of the line). One solution was to take the graphs x ↦ sin(a x) and another graphs x ↦ sin(x + a), both suitably parametrized by a.

The third problem was in fact harder. It involved proving informally but rigorously the statement:

􏰁(∀x,y∈A.φ(x,y)⇔(∃z∈A.ψ(x,z)∧ψ(z,y))􏰂 ⇒ (∃u∈A.ψ(u,u))⇒∃v∈A.φ(v,v)􏰂).

(It's less complicated than it looks and we did a lot of this systematically.) The second part asked for a counter-example to:

􏰁(∀x,y∈A.φ(x,y)⇔(∃z∈A.ψ(x,z)∧ψ(z,y))􏰂 ⇒ (∃v∈A.φ(v,v))⇒∃u∈A.ψ(u,u)􏰂)

I think they got scared by the formulas. But they don't get scared of scary intergrals in the analysis course!
Add a comment...

Andrej Bauer

Shared publicly  - 
 
I am looking for a PhD student in the area of homotopy type theory or design of proof assistants.

And did you know Ljubljana is second only to Greece as a top European destination according to Lonely Planet (http://www.lonelyplanet.com/europe/travel-tips-and-articles/lonely-planets-best-in-europe-2014)? It's one of the greenest and most livable cities in Europe.

#HomotopyTypeTheory   #scholarship  
I am looking for a PhD student in mathematics. Full tuition & stipend will be provided for a period of three years, which is also the official length of the programme. The topic of research is somewhat flexible and varies from constructive models of homotopy type theory to development of a ...
12
6
Michael Witbrock's profile photoDependent Types's profile photoDan Ghica's profile photoMila Marian's profile photo
5 comments
 
Fixed the year, thanks +Aleš Bizjak .
Add a comment...

Andrej Bauer

Shared publicly  - 
 
Thanks to the #TEDx University of Ljubljana team for a great event yesterday. I am releasing the code, the images, and all the animations from my talk, plus some extra animations not shown in the talk. Enjoy!

I spoke about the Beauty of Roots as described by  +John Baez on his web page. I calculated the roots of polynomials with coefficients ±1 up to degree 26 and beat the current record by +Sam Derbyshire  by 2 degrees. The race is on!

#tedtalk   #mathematics  
12
5
Dale Miller's profile photoDave Gordon's profile photogeorge oloo's profile photoMila Marian's profile photo
3 comments
 
Cool, thank you +Andrej Bauer! Now i'm left with the task to find out how i could have come up with your explanation myself. Reason to look at it many more times. Beautiful thing!
Add a comment...
People
Have him in circles
761 people
Dan Farmer's profile photo
khaled bhuyain's profile photo
Frederick Kintanar's profile photo
Gregor Cerinšek's profile photo
Michael Witbrock's profile photo
Peter Kuzma's profile photo
a bahari's profile photo
Noam Zeilberger's profile photo
Irma Walter's profile photo
Work
Employment
  • University of Ljubljana
    Professor, present
Places
Map of the places this user has livedMap of the places this user has livedMap of the places this user has lived
Currently
Ljubljana, Slovenia
Previously
Pittsburgh, USA - Duino, Italy
Links
Other profiles
Contributor to
Story
Tagline
Human.
Education
  • United World College of the Adriatic
    1988 - 1990
  • Univerza v Ljubljani
    mathematics, 1990 - 1994
  • Carnegie Mellon University
    logic, 1994 - 2000
Basic Information
Gender
Male